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

Theorem biimpar 471
 Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
Ref Expression
biimpa.1 (φ → (ψχ))
Assertion
Ref Expression
biimpar ((φ χ) → ψ)

Proof of Theorem biimpar
StepHypRef Expression
1 biimpa.1 . . 3 (φ → (ψχ))
21biimprd 214 . 2 (φ → (χψ))
32imp 418 1 ((φ χ) → ψ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-an 360 This theorem is referenced by:  exbiri  605  bitr  689  oplem1  930  eqtr  2370  funfni  5183  fnco  5191  fnssres  5196  fnimadisj  5203  foco  5279  f1ores  5300  foimacnv  5303  fvelimab  5370  dff3  5420  dffo4  5423  f1o2d  5727  ecelqsg  5979  elqsn0  5993  peano4nc  6150  ncspw1eu  6159  ce0addcnnul  6179  sbth  6206  dflec2  6210  ce0lenc1  6239  ncfin  6247
 Copyright terms: Public domain W3C validator