Theorem biimpar 285

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 151	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	imp 119	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105

This theorem depends on definitions:  df-bi 114

This theorem is referenced by:  exbiri  368  bitr  449  eqtr  2073  opabss  3848  euotd  4018  wetriext  4328  sosng  4440  xpsspw  4477  brcogw  4531  funimaexglem  5009  funfni  5026  fnco  5034  fnssres  5039  fn0  5045  fnimadisj  5046  fnimaeq0  5047  foco  5143  foimacnv  5171  fvelimab  5256  fvopab3ig  5273  dff3im  5339  dffo4  5342  fmptco  5357  f1eqcocnv  5458  f1ocnv2d  5731  fnexALT  5767  xp1st  5819  xp2nd  5820  tfrlemiubacc  5974  tfri2d  5980  tfri3  5983  ecelqsg  6189  elqsn0m  6204  fidifsnen  6361  recclnq  6547  nq0a0  6612  qreccl  8673  difelfzle  9093  modifeq2int  9330  frec2uzlt2d  9348  caucvgrelemcau  9800  recvalap  9916  fzomaxdiflem  9931  divconjdvds  10153