Theorem biimpac 478

Description: Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)

Hypothesis

Ref	Expression
biimpa.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpac	⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Proof of Theorem biimpac

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpcd 249	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 406	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  r19.29r  3102  gencbvex2  3489  2reu5  3705  ifpprsnss  4709  dfiun2g  4973  poltletr  6089  ordnbtwn  6412  funopsn  7095  onsucuni2  7778  1stconst  8043  2ndconst  8044  smo11  8297  omlimcl  8506  omxpenlem  9009  fodomr  9059  f1oenfirn  9107  f1domfi  9108  fodomfib  9232  fodomfibOLD  9234  infsupprpr  9412  r1val1  9701  alephval3  10023  dfac5lem4  10039  dfac5lem4OLD  10041  dfac5  10042  axdc4lem  10368  fodomb  10439  distrlem1pr  10939  map2psrpr  11024  supsrlem  11025  eqle  11239  swrd0  14612  repswswrd  14737  cshwidxmod  14756  rtrclind  15018  sumz  15675  prod1  15900  divalglem8  16360  flodddiv4  16375  pospo  18300  mgm2nsgrplem2  18881  eqg0subg  19162  rhmdvdsr  20476  lsmcv  21131  sraring  21173  opsrtoslem1  22043  madugsum  22618  hauscmplem  23381  bwth  23385  ptbasfi  23556  hmphindis  23772  fbncp  23814  fgcl  23853  fixufil  23897  uffixfr  23898  mbfima  25607  mbfimaicc  25608  ig1pdvds  26155  zabsle1  27273  tgldimor  28584  ax5seglem4  29015  axcontlem2  29048  axcontlem4  29050  nbgrval  29419  cusgrfi  29542  fusgrregdegfi  29653  rusgr1vtxlem  29671  wlkiswwlksupgr2  29960  elwwlks2ons3  30038  clwwlknonwwlknonb  30191  eucrctshift  30328  spansncvi  31738  eigposi  31922  pjnormssi  32254  sumdmdlem  32504  tngdim  33773  bnj168  34889  bnj964  35101  bnj966  35102  bnj1398  35192  fnrelpredd  35250  lfuhgr3  35318  acycgrislfgr  35350  cgrdegen  36202  btwnconn1lem11  36295  btwnconn1lem12  36296  btwnconn1lem14  36298  bj-opelidb1  37483  bj-inexeqex  37484  bj-idreseqb  37493  bj-ideqg1ALT  37495  bj-ccinftydisj  37543  phpreu  37939  fin2so  37942  matunitlindflem2  37952  poimirlem26  37981  poimirlem28  37983  dvasin  38039  isbnd2  38118  atcvrj0  39888  paddasslem5  40284  expeq1d  42770  pm13.13a  44852  iotavalb  44875  suctrALTcf  45366  suctrALTcfVD  45367  suctrALT3  45368  unisnALT  45370  2sb5ndALT  45376  xreqle  45768  supminfxr2  45915  fourierdlem40  46593  fourierdlem78  46630  tz6.12-afv2  47700  afv2fv0  47725  2ffzoeq  47788  clnbgrval  48310  dfsclnbgr6  48346  uspgrlimlem1  48476  uspgropssxp  48632  uspgrsprfo  48636  nn0sumshdiglemA  49107  itscnhlc0yqe  49247