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

Theorem orbi12i 680
 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 678 . 2 ((φ χ) ↔ (φ θ))
3 orbi12i.1 . . 3 (φψ)
43orbi1i 679 . 2 ((φ θ) ↔ (ψ θ))
52, 4bitri 173 1 ((φ χ) ↔ (ψ θ))
 Colors of variables: wff set class Syntax hints:   ↔ wb 98   ∨ wo 628 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 629 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  andir  731  anddi  733  dcbii  746  3orbi123i  1093  3or6  1217  excxor  1268  19.33b2  1517  sbequilem  1716  sborv  1767  sbor  1825  r19.43  2462  rexun  3117  indi  3178  difindiss  3185  symdifxor  3197  unab  3198  dfpr2  3383  rabrsndc  3429  pwprss  3567  pwtpss  3568  unipr  3585  uniun  3590  iunun  3725  iunxun  3726  brun  3801  pwunss  4011  ordsoexmid  4240  opthprc  4334  cnvsom  4804  ftpg  5290  tpostpos  5820  ltexprlemloc  6581  axpre-ltwlin  6767  axpre-apti  6769  axpre-mulext  6772
 Copyright terms: Public domain W3C validator