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

Theorem orbi12d 707
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 705 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 orbi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43orbi2d 704 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 177 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wo 629
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 630
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm4.39  735  dcbid  748  3orbi123d  1206  dfbi3dc  1288  eueq3dc  2715  sbcor  2807  sbcorg  2808  unjust  2921  elun  3084  ifbi  3348  elprg  3395  eltpg  3416  rabrsndc  3438  preq12bg  3544  swopolem  4042  soeq1  4052  sowlin  4057  ordtri2orexmid  4248  regexmidlemm  4257  regexmidlem1  4258  reg2exmidlema  4259  ordsoexmid  4286  ordtri2or2exmid  4296  nn0suc  4327  nndceq0  4339  0elnn  4340  soinxp  4410  fununi  4967  funcnvuni  4968  fun11iun  5147  unpreima  5292  isosolem  5463  xporderlem  5852  poxp  5853  frec0g  5983  frecsuclem3  5990  frecsuc  5991  indpi  6438  ltexprlemloc  6703  addextpr  6717  ltsosr  6847  aptisr  6861  mulextsr1lem  6862  mulextsr1  6863  axpre-ltwlin  6955  axpre-apti  6957  axpre-mulext  6960  axltwlin  7085  axapti  7088  reapval  7565  reapti  7568  reapmul1lem  7583  reapmul1  7584  reapadd1  7585  reapneg  7586  reapcotr  7587  remulext1  7588  apreim  7592  apsym  7595  apcotr  7596  apadd1  7597  addext  7599  apneg  7600  nn1m1nn  7930  nn1gt1  7945  elznn0  8258  elz2  8310  nn0n0n1ge2b  8318  nneoor  8338  uztric  8492  ltxr  8693  fzsplit2  8912  uzsplit  8952  fzospliti  9030  fzouzsplit  9033  sq11ap  9412  sqrt11ap  9634  abs00ap  9658  sumeq1  9872  bj-dcbi  10046  bj-nn0suc0  10073  bj-inf2vnlem2  10094  bj-nn0sucALT  10101
  Copyright terms: Public domain W3C validator