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

Theorem orbi12i 681
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 679 . 2 ((𝜑𝜒) ↔ (𝜑𝜃))
3 orbi12i.1 . . 3 (𝜑𝜓)
43orbi1i 680 . 2 ((𝜑𝜃) ↔ (𝜓𝜃))
52, 4bitri 173 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wb 98  wo 629
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  andir  732  anddi  734  dcbii  747  3orbi123i  1094  3or6  1218  excxor  1269  19.33b2  1520  sbequilem  1719  sborv  1770  sbor  1828  r19.43  2468  rexun  3123  indi  3184  difindiss  3191  symdifxor  3203  unab  3204  dfpr2  3394  rabrsndc  3438  pwprss  3576  pwtpss  3577  unipr  3594  uniun  3599  iunun  3734  iunxun  3735  brun  3810  pwunss  4020  ordsoexmid  4286  onintexmid  4297  opthprc  4391  cnvsom  4861  ftpg  5347  tpostpos  5879  ltexprlemloc  6703  axpre-ltwlin  6955  axpre-apti  6957  axpre-mulext  6960
  Copyright terms: Public domain W3C validator