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  2033  opabss  3787  euotd  3957  sosng  4331  xpsspw  4368  brcogw  4422  funimaexglem  4899  funfni  4916  fnco  4924  fnssres  4929  fn0  4935  fnimadisj  4936  fnimaeq0  4937  foco  5032  foimacnv  5060  fvelimab  5145  fvopab3ig  5162  dff3im  5228  dffo4  5231  fmptco  5246  f1eqcocnv  5347  f1ocnv2d  5618  fnexALT  5654  xp1st  5706  xp2nd  5707  tfrlemiubacc  5856  tfri2d  5863  tfri3  5866  ecelqsg  6061  elqsn0m  6076  recclnq  6240  nq0a0  6301  qreccl  8061