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

Theorem orbi12i 722
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 720 . 2 ((𝜑𝜒) ↔ (𝜑𝜃))
3 orbi12i.1 . . 3 (𝜑𝜓)
43orbi1i 721 . 2 ((𝜑𝜃) ↔ (𝜓𝜃))
52, 4bitri 183 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wb 104  wo 670
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  andir  774  anddi  776  dcbii  791  3orbi123i  1139  3or6  1269  excxor  1324  19.33b2  1576  sbequilem  1777  sborv  1829  sbor  1888  r19.43  2547  rexun  3203  indi  3270  difindiss  3277  symdifxor  3289  unab  3290  dfpr2  3493  rabrsndc  3538  pwprss  3679  pwtpss  3680  unipr  3697  uniun  3702  iunun  3838  iunxun  3839  brun  3921  pwunss  4143  ordsoexmid  4415  onintexmid  4425  dcextest  4433  opthprc  4528  cnvsom  5018  ftpg  5536  tpostpos  6091  eldju  6868  djur  6869  ltexprlemloc  7316  axpre-ltwlin  7568  axpre-apti  7570  axpre-mulext  7573  fz01or  9732  cbvsum  10968  fsum3  10995  gcdsupex  11441  gcdsupcl  11442
  Copyright terms: Public domain W3C validator