Theorem biimpac 477

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 405	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 395

This theorem is referenced by:  r19.29r  3114  gencbvex2  3535  2reu5  3753  ifpprsnss  4767  dfiun2g  5032  poltletr  6132  ordnbtwn  6456  tz6.12-1OLD  6914  funopsn  7147  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  25379  mbfimaicc  25380  ig1pdvds  25929  zabsle1  27035  tgldimor  28020  ax5seglem4  28457  axcontlem2  28490  axcontlem4  28492  nbgrval  28860  cusgrfi  28982  fusgrregdegfi  29093  rusgr1vtxlem  29111  wlkiswwlksupgr2  29398  elwwlks2ons3  29476  clwwlknonwwlknonb  29626  eucrctshift  29763  spansncvi  31172  eigposi  31356  pjnormssi  31688  sumdmdlem  31938  tngdim  32986  bnj168  34039  bnj964  34252  bnj966  34253  bnj1398  34343  fnrelpredd  34390  lfuhgr3  34408  acycgrislfgr  34441  cgrdegen  35280  btwnconn1lem11  35373  btwnconn1lem12  35374  btwnconn1lem14  35376  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  44326  supminfxr2  44477  fourierdlem40  45161  fourierdlem78  45198  tz6.12-afv2  46246  afv2fv0  46271  2ffzoeq  46334  uspgropssxp  46820  uspgrsprfo  46824  difmodm1lt  47295  nn0sumshdiglemA  47392  itscnhlc0yqe  47532