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

Theorem orbi12i 736
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 734 . 2  |-  ( (
ph  \/  ch )  <->  (
ph  \/  th )
)
3 orbi12i.1 . . 3  |-  ( ph  <->  ps )
43orbi1i 735 . 2  |-  ( (
ph  \/  th )  <->  ( ps  \/  th )
)
52, 4bitri 183 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  th )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 104    \/ wo 680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  andir  791  anddi  793  3orbi123i  1154  3or6  1284  excxor  1339  19.33b2  1591  sbequilem  1792  sborv  1844  sbor  1903  r19.43  2564  rexun  3224  indi  3291  difindiss  3298  symdifxor  3310  unab  3311  dfpr2  3514  rabrsndc  3559  pwprss  3700  pwtpss  3701  unipr  3718  uniun  3723  iunun  3859  iunxun  3860  brun  3947  pwunss  4173  ordsoexmid  4445  onintexmid  4455  dcextest  4463  opthprc  4558  cnvsom  5050  ftpg  5570  tpostpos  6127  eldju  6919  djur  6920  ltexprlemloc  7379  axpre-ltwlin  7655  axpre-apti  7657  axpre-mulext  7660  axpre-suploc  7674  fz01or  9842  cbvsum  11080  fsum3  11107  gcdsupex  11553  gcdsupcl  11554
  Copyright terms: Public domain W3C validator