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

Theorem orbi12d 740
Description: Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
orbi12d.1  |-  ( ph  ->  ( ps  <->  ch )
)
orbi12d.2  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
orbi12d  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  ta ) ) )

Proof of Theorem orbi12d
StepHypRef Expression
1 orbi12d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21orbi1d 738 . 2  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  th ) ) )
3 orbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43orbi2d 737 . 2  |-  ( ph  ->  ( ( ch  \/  th )  <->  ( ch  \/  ta ) ) )
52, 4bitrd 186 1  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103    \/ wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm4.39  769  dcbid  782  3orbi123d  1243  dfbi3dc  1329  eueq3dc  2775  sbcor  2867  sbcorg  2868  unjust  2985  elun  3123  ifbi  3386  elprg  3436  eltpg  3456  rabrsndc  3478  preq12bg  3585  exmid01  3988  swopolem  4088  soeq1  4098  sowlin  4103  ordtri2orexmid  4294  regexmidlemm  4303  regexmidlem1  4304  reg2exmidlema  4305  ordsoexmid  4333  ordtri2or2exmid  4342  nn0suc  4373  nndceq0  4385  0elnn  4386  soinxp  4456  fununi  5018  funcnvuni  5019  fun11iun  5198  unpreima  5344  isosolem  5514  xporderlem  5903  poxp  5904  frec0g  6066  freccllem  6071  frecfcllem  6073  frecsuclem  6075  frecsuc  6076  inffiexmid  6457  indpi  6646  ltexprlemloc  6911  addextpr  6925  ltsosr  7055  aptisr  7069  mulextsr1lem  7070  mulextsr1  7071  axpre-ltwlin  7163  axpre-apti  7165  axpre-mulext  7168  axltwlin  7299  axapti  7302  reapval  7795  reapti  7798  reapmul1lem  7813  reapmul1  7814  reapadd1  7815  reapneg  7816  reapcotr  7817  remulext1  7818  apreim  7822  apsym  7825  apcotr  7826  apadd1  7827  addext  7829  apneg  7830  nn1m1nn  8176  nn1gt1  8191  elznn0  8499  elz2  8552  nn0n0n1ge2b  8560  nneoor  8582  uztric  8773  ltxr  8979  fzsplit2  9197  uzsplit  9237  fzospliti  9314  fzouzsplit  9317  exbtwnzlemstep  9386  exbtwnzlemex  9388  qavgle  9397  frec2uzled  9563  sq11ap  9788  sqrt11ap  10125  abs00ap  10149  maxclpr  10309  minmax  10313  sumeq1  10393  sumeq2d  10397  sumeq2  10398  fz1f1o  10399  zeo3  10475  odd2np1lem  10479  dvdsprime  10711  coprm  10730  decidi  10865  bj-dcbi  10986  bj-nn0suc0  11012  bj-inf2vnlem2  11033  bj-nn0sucALT  11040
  Copyright terms: Public domain W3C validator