NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  orbi1i GIF version

Theorem orbi1i 506
Description: Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
orbi2i.1 (φψ)
Assertion
Ref Expression
orbi1i ((φ χ) ↔ (ψ χ))

Proof of Theorem orbi1i
StepHypRef Expression
1 orcom 376 . 2 ((φ χ) ↔ (χ φ))
2 orbi2i.1 . . 3 (φψ)
32orbi2i 505 . 2 ((χ φ) ↔ (χ ψ))
4 orcom 376 . 2 ((χ ψ) ↔ (ψ χ))
51, 3, 43bitri 262 1 ((φ χ) ↔ (ψ χ))
Colors of variables: wff setvar class
Syntax hints:  wb 176   wo 357
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177  df-or 359
This theorem is referenced by:  orbi12i  507  orordi  516  3anor  948  3or6  1263  19.45  1878  unass  3420  dfimak2  4298  ssfin  4470  eqtfinrelk  4486  evenoddnnnul  4514  nmembers1lem3  6270  nncdiv3  6277  nchoicelem6  6294  nchoicelem9  6297  nchoicelem18  6306
  Copyright terms: Public domain W3C validator