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  3096  gencbvex2  3508  2reu5  3729  ifpprsnss  4728  dfiun2g  4994  poltletr  6105  ordnbtwn  6427  tz6.12-1OLD  6882  funopsn  7120  onsucuni2  7809  1stconst  8079  2ndconst  8080  smo11  8333  omlimcl  8542  omxpenlem  9042  fodomr  9092  f1oenfirn  9144  f1domfi  9145  fodomfib  9280  fodomfibOLD  9282  infsupprpr  9457  r1val1  9739  alephval3  10063  dfac5lem4  10079  dfac5lem4OLD  10081  dfac5  10082  axdc4lem  10408  fodomb  10479  distrlem1pr  10978  map2psrpr  11063  supsrlem  11064  eqle  11276  swrd0  14623  repswswrd  14749  cshwidxmod  14768  rtrclind  15031  sumz  15688  prod1  15910  divalglem8  16370  flodddiv4  16385  pospo  18304  mgm2nsgrplem2  18846  eqg0subg  19128  rhmdvdsr  20417  lsmcv  21051  sraring  21093  opsrtoslem1  21962  madugsum  22530  hauscmplem  23293  bwth  23297  ptbasfi  23468  hmphindis  23684  fbncp  23726  fgcl  23765  fixufil  23809  uffixfr  23810  mbfima  25531  mbfimaicc  25532  ig1pdvds  26085  zabsle1  27207  tgldimor  28429  ax5seglem4  28859  axcontlem2  28892  axcontlem4  28894  nbgrval  29263  cusgrfi  29386  fusgrregdegfi  29497  rusgr1vtxlem  29515  wlkiswwlksupgr2  29807  elwwlks2ons3  29885  clwwlknonwwlknonb  30035  eucrctshift  30172  spansncvi  31581  eigposi  31765  pjnormssi  32097  sumdmdlem  32347  tngdim  33609  bnj168  34720  bnj964  34933  bnj966  34934  bnj1398  35024  fnrelpredd  35079  lfuhgr3  35107  acycgrislfgr  35139  cgrdegen  35992  btwnconn1lem11  36085  btwnconn1lem12  36086  btwnconn1lem14  36088  bj-opelidb1  37141  bj-inexeqex  37142  bj-idreseqb  37151  bj-ideqg1ALT  37153  bj-ccinftydisj  37201  phpreu  37598  fin2so  37601  matunitlindflem2  37611  poimirlem26  37640  poimirlem28  37642  dvasin  37698  isbnd2  37777  atcvrj0  39422  paddasslem5  39818  expeq1d  42312  pm13.13a  44396  iotavalb  44419  suctrALTcf  44911  suctrALTcfVD  44912  suctrALT3  44913  unisnALT  44915  2sb5ndALT  44921  xreqle  45315  supminfxr2  45465  fourierdlem40  46145  fourierdlem78  46182  tz6.12-afv2  47241  afv2fv0  47266  2ffzoeq  47328  clnbgrval  47823  dfsclnbgr6  47858  uspgrlimlem1  47987  uspgropssxp  48132  uspgrsprfo  48136  nn0sumshdiglemA  48608  itscnhlc0yqe  48748