Theorem biimpac 479

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  r19.29r  3103  gencbvex2  3489  2reu5  3699  ifpprsnss  4696  dfiun2g  4959  poltletr  6082  ordnbtwn  6405  funopsn  7090  funopsnOLD  7091  onsucuni2  7774  1stconst  8039  2ndconst  8040  smo11  8294  omlimcl  8503  omxpenlem  9006  fodomr  9056  f1oenfirn  9104  f1domfi  9105  fodomfib  9229  fodomfibOLD  9231  infsupprpr  9409  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  20480  lsmcv  21134  sraring  21176  opsrtoslem1  22031  madugsum  22626  hauscmplem  23389  bwth  23393  ptbasfi  23564  hmphindis  23780  fbncp  23822  fgcl  23861  fixufil  23905  uffixfr  23906  mbfima  25615  mbfimaicc  25616  ig1pdvds  26163  zabsle1  27277  tgldimor  28588  ax5seglem4  29019  axcontlem2  29052  axcontlem4  29054  nbgrval  29423  cusgrfi  29545  fusgrregdegfi  29656  rusgr1vtxlem  29674  wlkiswwlksupgr2  29963  elwwlks2ons3  30041  clwwlknonwwlknonb  30194  eucrctshift  30331  spansncvi  31741  eigposi  31925  pjnormssi  32257  sumdmdlem  32507  tngdim  33797  bnj168  34913  bnj964  35125  bnj966  35126  bnj1398  35216  fnrelpredd  35272  lfuhgr3  35348  acycgrislfgr  35380  cgrdegen  36232  btwnconn1lem11  36325  btwnconn1lem12  36326  btwnconn1lem14  36328  bj-opelidb1  37513  bj-inexeqex  37514  bj-idreseqb  37523  bj-ideqg1ALT  37525  bj-ccinftydisj  37573  phpreu  37971  fin2so  37974  matunitlindflem2  37984  poimirlem26  38013  poimirlem28  38015  dvasin  38071  isbnd2  38150  atcvrj0  39920  paddasslem5  40316  expeq1d  42801  pm13.13a  44851  iotavalb  44874  suctrALTcf  45365  suctrALTcfVD  45366  suctrALT3  45367  unisnALT  45369  2sb5ndALT  45375  xreqle  45765  supminfxr2  45912  fourierdlem40  46590  fourierdlem78  46627  tz6.12-afv2  47703  afv2fv0  47728  2ffzoeq  47791  clnbgrval  48313  dfsclnbgr6  48349  uspgrlimlem1  48479  uspgropssxp  48635  uspgrsprfo  48639  nn0sumshdiglemA  49110  itscnhlc0yqe  49250