Theorem biimpar 297

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exbiri  382  bitr  472  biadanid  616  eqtr  2247  opabss  4147  euotd  4340  wetriext  4668  sosng  4791  xpsspw  4830  brcogw  4890  funimaexglem  5403  funfni  5422  fnco  5430  fnssres  5435  fn0  5442  fnimadisj  5443  fnimaeq0  5444  foco  5558  foimacnv  5589  fvelimab  5689  fvopab3ig  5707  dff3im  5779  dffo4  5782  fmptco  5800  f1eqcocnv  5914  f1ocnv2d  6208  fnexALT  6254  xp1st  6309  xp2nd  6310  tfrlemiubacc  6474  tfri2d  6480  tfr1onlemubacc  6490  tfrcllemubacc  6503  tfri3  6511  ecelqsg  6733  elqsn0m  6748  fidifsnen  7028  pr1or2  7363  recclnq  7575  nq0a0  7640  qreccl  9833  difelfzle  10326  exfzdc  10441  zsupcllemstep  10444  modifeq2int  10603  frec2uzlt2d  10621  zzlesq  10925  1elfz0hash  11023  lennncl  11086  wrdsymb0  11099  ccatsymb  11132  ccatlid  11136  ccatass  11138  ccatswrd  11197  swrdccat2  11198  ccatpfx  11228  swrdccatfn  11251  swrdccat  11262  caucvgrelemcau  11486  recvalap  11603  fzomaxdiflem  11618  2zsupmax  11732  2zinfmin  11749  fsumparts  11976  ntrivcvgap  12054  fsumdvds  12348  divconjdvds  12355  ndvdssub  12436  rplpwr  12543  dvdssqlem  12546  eucalgcvga  12575  mulgcddvds  12611  isprm2lem  12633  powm2modprm  12770  coprimeprodsq  12775  pythagtriplem11  12792  pythagtriplem13  12794  pcadd2  12859  4sqlem11  12919  grpidd  13411  ismndd  13465  gsumfzz  13523  gsumwmhm  13526  mulgaddcom  13678  resghm  13792  conjnsg  13813  isrngd  13911  isringd  13999  01eq0ring  14147  lspsneq0b  14385  lmodindp1  14386  znf1o  14609  psrgrp  14643  uniopn  14669  ntrval  14778  clsval  14779  neival  14811  restdis  14852  lmbrf  14883  cnpnei  14887  dviaddf  15373  dvimulf  15374  logbgt0b  15634  perfectlem2  15668  lgslem4  15676  lgsmod  15699  lgsdir2lem2  15702  lgsdir2  15706  lgsne0  15711  lgsmulsqcoprm  15719  lgseisenlem1  15743  2lgsoddprm  15786  2sqlem4  15791