Theorem biimpar 291

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  exbiri  374  bitr  456  eqtr  2100  opabss  3862  euotd  4037  wetriext  4347  sosng  4459  xpsspw  4498  brcogw  4552  funimaexglem  5033  funfni  5050  fnco  5058  fnssres  5063  fn0  5069  fnimadisj  5070  fnimaeq0  5071  foco  5167  foimacnv  5195  fvelimab  5281  fvopab3ig  5298  dff3im  5364  dffo4  5367  fmptco  5382  f1eqcocnv  5482  f1ocnv2d  5755  fnexALT  5791  xp1st  5843  xp2nd  5844  tfrlemiubacc  5999  tfri2d  6005  tfr1onlemubacc  6015  tfrcllemubacc  6028  tfri3  6036  ecelqsg  6246  elqsn0m  6261  fidifsnen  6426  recclnq  6696  nq0a0  6761  qreccl  8860  difelfzle  9274  exfzdc  9378  modifeq2int  9520  frec2uzlt2d  9538  1elfz0hash  9882  caucvgrelemcau  10067  recvalap  10184  fzomaxdiflem  10199  divconjdvds  10457  ndvdssub  10537  zsupcllemstep  10548  rplpwr  10623  dvdssqlem  10626  eucialgcvga  10647  mulgcddvds  10683  isprm2lem  10705