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

Theorem orbi12i 754
 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 752 . 2 ((𝜑𝜒) ↔ (𝜑𝜃))
3 orbi12i.1 . . 3 (𝜑𝜓)
43orbi1i 753 . 2 ((𝜑𝜃) ↔ (𝜓𝜃))
52, 4bitri 183 1 ((𝜑𝜒) ↔ (𝜓𝜃))
 Colors of variables: wff set class Syntax hints:   ↔ wb 104   ∨ wo 698 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  andir  809  anddi  811  3orbi123i  1172  3or6  1302  excxor  1357  19.33b2  1609  sbequilem  1811  sborv  1863  sbor  1928  r19.43  2592  rexun  3260  indi  3327  difindiss  3334  symdifxor  3346  unab  3347  dfpr2  3550  rabrsndc  3598  pwprss  3739  pwtpss  3740  unipr  3757  uniun  3762  iunun  3898  iunxun  3899  brun  3986  pwunss  4212  ordsoexmid  4484  onintexmid  4494  dcextest  4502  opthprc  4597  cnvsom  5089  ftpg  5611  tpostpos  6168  eldju  6960  djur  6961  ltexprlemloc  7438  axpre-ltwlin  7714  axpre-apti  7716  axpre-mulext  7719  axpre-suploc  7733  fz01or  9921  cbvsum  11160  fsum3  11187  cbvprod  11358  gcdsupex  11680  gcdsupcl  11681
 Copyright terms: Public domain W3C validator