ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  orbi12i GIF 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  1761  sborv  1813  sbor  1871  r19.43  2518  rexun  3164  indi  3229  difindiss  3236  symdifxor  3248  unab  3249  dfpr2  3441  rabrsndc  3484  pwprss  3623  pwtpss  3624  unipr  3641  uniun  3646  iunun  3781  iunxun  3782  brun  3857  pwunss  4074  ordsoexmid  4341  onintexmid  4351  dcextest  4359  opthprc  4447  cnvsom  4928  ftpg  5423  tpostpos  5961  eldju  6666  ltexprlemloc  7069  axpre-ltwlin  7321  axpre-apti  7323  axpre-mulext  7326  fz01or  9418  gcdsupex  10729  gcdsupcl  10730
  Copyright terms: Public domain W3C validator