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

Theorem orbi12i 738
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 736 . 2  |-  ( (
ph  \/  ch )  <->  (
ph  \/  th )
)
3 orbi12i.1 . . 3  |-  ( ph  <->  ps )
43orbi1i 737 . 2  |-  ( (
ph  \/  th )  <->  ( ps  \/  th )
)
52, 4bitri 183 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  th )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 104    \/ wo 682
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 683
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  andir  793  anddi  795  3orbi123i  1156  3or6  1286  excxor  1341  19.33b2  1593  sbequilem  1794  sborv  1846  sbor  1905  r19.43  2566  rexun  3226  indi  3293  difindiss  3300  symdifxor  3312  unab  3313  dfpr2  3516  rabrsndc  3561  pwprss  3702  pwtpss  3703  unipr  3720  uniun  3725  iunun  3861  iunxun  3862  brun  3949  pwunss  4175  ordsoexmid  4447  onintexmid  4457  dcextest  4465  opthprc  4560  cnvsom  5052  ftpg  5572  tpostpos  6129  eldju  6921  djur  6922  ltexprlemloc  7383  axpre-ltwlin  7659  axpre-apti  7661  axpre-mulext  7664  axpre-suploc  7678  fz01or  9846  cbvsum  11084  fsum3  11111  gcdsupex  11558  gcdsupcl  11559
  Copyright terms: Public domain W3C validator