ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  orbi12d Structured version   GIF version

Theorem orbi12d 694
Description: Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
orbi12d.1 (φ → (ψχ))
orbi12d.2 (φ → (θτ))
Assertion
Ref Expression
orbi12d (φ → ((ψ θ) ↔ (χ τ)))

Proof of Theorem orbi12d
StepHypRef Expression
1 orbi12d.1 . . 3 (φ → (ψχ))
21orbi1d 692 . 2 (φ → ((ψ θ) ↔ (χ θ)))
3 orbi12d.2 . . 3 (φ → (θτ))
43orbi2d 691 . 2 (φ → ((χ θ) ↔ (χ τ)))
52, 4bitrd 177 1 (φ → ((ψ θ) ↔ (χ τ)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   wo 616
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm4.39  723  dcbid  739  3orbi123d  1191  dfbi3dc  1271  eueq3dc  2692  sbcor  2784  sbcorg  2785  unjust  2898  elun  3061  ifbi  3325  elprg  3367  eltpg  3390  rabrsndc  3412  preq12bg  3518  swopolem  4016  soeq1  4026  sowlin  4031  ordtri2orexmid  4195  regexmidlemm  4201  regexmidlem1  4202  ordsoexmid  4224  nn0suc  4254  nndceq0  4266  0elnn  4267  soinxp  4337  fununi  4893  funcnvuni  4894  fun11iun  5072  unpreima  5217  isosolem  5388  xporderlem  5774  poxp  5775  frec0g  5902  frecsuclem3  5906  frecsuc  5907  ltexprlemloc  6444  ltsosr  6511  axpre-ltwlin  6577  axltwlin  6688  bj-d0clsepcl  7295  bj-nn0suc0  7319  bj-inf2vnlem2  7336  bj-nn0sucALT  7343
  Copyright terms: Public domain W3C validator