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

Theorem orbi2i 505
Description: Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.)
Hypothesis
Ref Expression
orbi2i.1 (φψ)
Assertion
Ref Expression
orbi2i ((χ φ) ↔ (χ ψ))

Proof of Theorem orbi2i
StepHypRef Expression
1 orbi2i.1 . . . 4 (φψ)
21biimpi 186 . . 3 (φψ)
32orim2i 504 . 2 ((χ φ) → (χ ψ))
41biimpri 197 . . 3 (ψφ)
54orim2i 504 . 2 ((χ ψ) → (χ φ))
63, 5impbii 180 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:  orbi1i  506  orbi12i  507  orass  510  or4  514  or42  515  orordir  517  dn1  932  3orcomb  944  excxor  1309  cad1  1398  nf4  1868  19.44  1877  exmidne  2522  r19.30  2756  sspsstri  3371  unass  3420  undi  3502  undif3  3515  undif4  3607  ssunpr  3868  sspr  3869  sstp  3870  iinun2  4032  iinuni  4049  axtyplowerprim  4094  pwadjoin  4119  nnsucelrlem2  4425  ltfintrilem1  4465  nnadjoin  4520  dfphi2  4569  phi011lem1  4598  clos1baseima  5883  clos1basesucg  5884  fce  6188
  Copyright terms: Public domain W3C validator