Theorem biimpar 281

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

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	biimprd 147	. 2 ⊢ (φ → (χ → ψ))
3	2	imp 115	1 ⊢ ((φ ∧ χ) → ψ)

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  exbiri  364  bitr  441  eqtr  2054  opabss  3812  euotd  3982  sosng  4356  xpsspw  4393  brcogw  4447  funimaexglem  4925  funfni  4942  fnco  4950  fnssres  4955  fn0  4961  fnimadisj  4962  fnimaeq0  4963  foco  5059  foimacnv  5087  fvelimab  5172  fvopab3ig  5189  dff3im  5255  dffo4  5258  fmptco  5273  f1eqcocnv  5374  f1ocnv2d  5646  fnexALT  5682  xp1st  5734  xp2nd  5735  tfrlemiubacc  5885  tfri2d  5891  tfri3  5894  ecelqsg  6095  elqsn0m  6110  recclnq  6376  nq0a0  6440  qreccl  8351  difelfzle  8762  frec2uzlt2d  8871