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

Theorem orbi12i 714
Description: Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
orbi12i.1  |-  ( ph  <->  ps )
orbi12i.2  |-  ( ch  <->  th )
Assertion
Ref Expression
orbi12i  |-  ( (
ph  \/  ch )  <->  ( ps  \/  th )
)

Proof of Theorem orbi12i
StepHypRef Expression
1 orbi12i.2 . . 3  |-  ( ch  <->  th )
21orbi2i 712 . 2  |-  ( (
ph  \/  ch )  <->  (
ph  \/  th )
)
3 orbi12i.1 . . 3  |-  ( ph  <->  ps )
43orbi1i 713 . 2  |-  ( (
ph  \/  th )  <->  ( ps  \/  th )
)
52, 4bitri 182 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  th )
)
Colors of variables: wff set class
Syntax hints:    <-> 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:  andir  766  anddi  768  dcbii  781  3orbi123i  1129  3or6  1255  excxor  1310  19.33b2  1561  sbequilem  1760  sborv  1812  sbor  1870  r19.43  2513  rexun  3153  indi  3218  difindiss  3225  symdifxor  3237  unab  3238  dfpr2  3425  rabrsndc  3468  pwprss  3605  pwtpss  3606  unipr  3623  uniun  3628  iunun  3763  iunxun  3764  brun  3839  pwunss  4046  ordsoexmid  4313  onintexmid  4323  opthprc  4417  cnvsom  4891  ftpg  5379  tpostpos  5913  ltexprlemloc  6859  axpre-ltwlin  7111  axpre-apti  7113  axpre-mulext  7116  fz01or  9204  gcdsupex  10493  gcdsupcl  10494
  Copyright terms: Public domain W3C validator