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  444  eqtr  2039  opabss  3795  euotd  3965  sosng  4340  xpsspw  4377  brcogw  4431  funimaexglem  4908  funfni  4925  fnco  4933  fnssres  4938  fn0  4944  fnimadisj  4945  fnimaeq0  4946  foco  5041  foimacnv  5069  fvelimab  5154  fvopab3ig  5171  dff3im  5237  dffo4  5240  fmptco  5255  f1eqcocnv  5356  f1ocnv2d  5627  fnexALT  5663  xp1st  5715  xp2nd  5716  tfrlemiubacc  5865  tfri2d  5872  tfri3  5875  ecelqsg  6070  elqsn0m  6085  recclnq  6251  nq0a0  6312