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

Theorem orbi12i 691
 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 689 . 2 ((𝜑𝜒) ↔ (𝜑𝜃))
3 orbi12i.1 . . 3 (𝜑𝜓)
43orbi1i 690 . 2 ((𝜑𝜃) ↔ (𝜓𝜃))
52, 4bitri 177 1 ((𝜑𝜒) ↔ (𝜓𝜃))
 Colors of variables: wff set class Syntax hints:   ↔ wb 102   ∨ wo 639 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  andir  743  anddi  745  dcbii  758  3orbi123i  1105  3or6  1229  excxor  1285  19.33b2  1536  sbequilem  1735  sborv  1786  sbor  1844  r19.43  2485  rexun  3150  indi  3211  difindiss  3218  symdifxor  3230  unab  3231  dfpr2  3421  rabrsndc  3465  pwprss  3603  pwtpss  3604  unipr  3621  uniun  3626  iunun  3761  iunxun  3762  brun  3837  pwunss  4047  ordsoexmid  4313  onintexmid  4324  opthprc  4418  cnvsom  4888  ftpg  5374  tpostpos  5909  ltexprlemloc  6762  axpre-ltwlin  7014  axpre-apti  7016  axpre-mulext  7019  fz01or  10189
 Copyright terms: Public domain W3C validator