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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397

This theorem is referenced by:  r19.29r  3116  gencbvex2  3536  2reu5  3754  ifpprsnss  4768  dfiun2g  5033  poltletr  6133  ordnbtwn  6457  tz6.12-1OLD  6915  funopsn  7148  onsucuni2  7824  1stconst  8088  2ndconst  8089  smo11  8366  omlimcl  8580  omxpenlem  9075  fodomr  9130  f1oenfirn  9185  f1domfi  9186  fodomfib  9328  infsupprpr  9501  r1val1  9783  alephval3  10107  dfac5lem4  10123  dfac5  10125  axdc4lem  10452  fodomb  10523  distrlem1pr  11022  map2psrpr  11107  supsrlem  11108  eqle  11320  swrd0  14612  repswswrd  14738  cshwidxmod  14757  rtrclind  15016  sumz  15672  prod1  15892  divalglem8  16347  flodddiv4  16360  pospo  18302  mgm2nsgrplem2  18836  eqg0subg  19111  rhmdvdsr  20399  lsmcv  20899  sraring  20953  psrbagfsuppOLD  21693  opsrtoslem1  21835  madugsum  22365  hauscmplem  23130  bwth  23134  ptbasfi  23305  hmphindis  23521  fbncp  23563  fgcl  23602  fixufil  23646  uffixfr  23647  mbfima  25371  mbfimaicc  25372  ig1pdvds  25918  zabsle1  27023  tgldimor  28008  ax5seglem4  28445  axcontlem2  28478  axcontlem4  28480  nbgrval  28848  cusgrfi  28970  fusgrregdegfi  29081  rusgr1vtxlem  29099  wlkiswwlksupgr2  29386  elwwlks2ons3  29464  clwwlknonwwlknonb  29614  eucrctshift  29751  spansncvi  31160  eigposi  31344  pjnormssi  31676  sumdmdlem  31926  tngdim  32974  bnj168  34027  bnj964  34240  bnj966  34241  bnj1398  34331  fnrelpredd  34378  lfuhgr3  34396  acycgrislfgr  34429  cgrdegen  35268  btwnconn1lem11  35361  btwnconn1lem12  35362  btwnconn1lem14  35364  bj-opelidb1  36337  bj-inexeqex  36338  bj-idreseqb  36347  bj-ideqg1ALT  36349  bj-ccinftydisj  36397  phpreu  36775  fin2so  36778  matunitlindflem2  36788  poimirlem26  36817  poimirlem28  36819  dvasin  36875  isbnd2  36954  atcvrj0  38602  paddasslem5  38998  pm13.13a  43468  iotavalb  43491  suctrALTcf  43985  suctrALTcfVD  43986  suctrALT3  43987  unisnALT  43989  2sb5ndALT  43995  xreqle  44327  supminfxr2  44478  fourierdlem40  45162  fourierdlem78  45199  tz6.12-afv2  46247  afv2fv0  46272  2ffzoeq  46335  uspgropssxp  46821  uspgrsprfo  46825  difmodm1lt  47296  nn0sumshdiglemA  47393  itscnhlc0yqe  47533