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

Theorem orbi12d 717
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 715 . 2  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  th ) ) )
3 orbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43orbi2d 714 . 2  |-  ( ph  ->  ( ( ch  \/  th )  <->  ( ch  \/  ta ) ) )
52, 4bitrd 181 1  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102    \/ wo 639
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  pm4.39  746  dcbid  759  3orbi123d  1217  dfbi3dc  1304  eueq3dc  2737  sbcor  2829  sbcorg  2830  unjust  2948  elun  3111  ifbi  3375  elprg  3422  eltpg  3443  rabrsndc  3465  preq12bg  3571  swopolem  4069  soeq1  4079  sowlin  4084  ordtri2orexmid  4275  regexmidlemm  4284  regexmidlem1  4285  reg2exmidlema  4286  ordsoexmid  4313  ordtri2or2exmid  4323  nn0suc  4354  nndceq0  4366  0elnn  4367  soinxp  4437  fununi  4994  funcnvuni  4995  fun11iun  5174  unpreima  5319  isosolem  5490  xporderlem  5879  poxp  5880  frec0g  6013  frecsuclem3  6020  frecsuc  6021  indpi  6497  ltexprlemloc  6762  addextpr  6776  ltsosr  6906  aptisr  6920  mulextsr1lem  6921  mulextsr1  6922  axpre-ltwlin  7014  axpre-apti  7016  axpre-mulext  7019  axltwlin  7145  axapti  7148  reapval  7640  reapti  7643  reapmul1lem  7658  reapmul1  7659  reapadd1  7660  reapneg  7661  reapcotr  7662  remulext1  7663  apreim  7667  apsym  7670  apcotr  7671  apadd1  7672  addext  7674  apneg  7675  nn1m1nn  8007  nn1gt1  8022  elznn0  8316  elz2  8369  nn0n0n1ge2b  8377  nneoor  8398  uztric  8589  ltxr  8795  fzsplit2  9015  uzsplit  9055  fzospliti  9133  fzouzsplit  9136  qavgle  9213  sq11ap  9576  sqrt11ap  9857  abs00ap  9881  sumeq1  10097  zeo3  10171  odd2np1lem  10175  bj-dcbi  10407  bj-nn0suc0  10434  bj-inf2vnlem2  10455  bj-nn0sucALT  10462
  Copyright terms: Public domain W3C validator