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
orbi12i.2
Assertion
Ref Expression
orbi12i

Proof of Theorem orbi12i
StepHypRef Expression
1 orbi12i.2 . . 3
21orbi2i 712 . 2
3 orbi12i.1 . . 3
43orbi1i 713 . 2
52, 4bitri 182 1
 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