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

Theorem orbi12i 716
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 714 . 2  |-  ( (
ph  \/  ch )  <->  (
ph  \/  th )
)
3 orbi12i.1 . . 3  |-  ( ph  <->  ps )
43orbi1i 715 . 2  |-  ( (
ph  \/  th )  <->  ( ps  \/  th )
)
52, 4bitri 182 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  th )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 103    \/ wo 664
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 665
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  andir  768  anddi  770  dcbii  785  3orbi123i  1133  3or6  1259  excxor  1314  19.33b2  1565  sbequilem  1766  sborv  1818  sbor  1876  r19.43  2525  rexun  3178  indi  3244  difindiss  3251  symdifxor  3263  unab  3264  dfpr2  3460  rabrsndc  3505  pwprss  3644  pwtpss  3645  unipr  3662  uniun  3667  iunun  3803  iunxun  3804  brun  3883  pwunss  4101  ordsoexmid  4368  onintexmid  4378  dcextest  4386  opthprc  4477  cnvsom  4961  ftpg  5465  tpostpos  6011  eldju  6738  ltexprlemloc  7145  axpre-ltwlin  7397  axpre-apti  7399  axpre-mulext  7402  fz01or  9492  cbvsum  10713  fisum  10742  gcdsupex  11042  gcdsupcl  11043
  Copyright terms: Public domain W3C validator