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  3502  2reu5  3718  ifpprsnss  4723  dfiun2g  4987  poltletr  6097  ordnbtwn  6420  funopsn  7103  onsucuni2  7786  1stconst  8052  2ndconst  8053  smo11  8306  omlimcl  8515  omxpenlem  9018  fodomr  9068  f1oenfirn  9116  f1domfi  9117  fodomfib  9241  fodomfibOLD  9243  infsupprpr  9421  r1val1  9710  alephval3  10032  dfac5lem4  10048  dfac5lem4OLD  10050  dfac5  10051  axdc4lem  10377  fodomb  10448  distrlem1pr  10948  map2psrpr  11033  supsrlem  11034  eqle  11247  swrd0  14594  repswswrd  14719  cshwidxmod  14738  rtrclind  15000  sumz  15657  prod1  15879  divalglem8  16339  flodddiv4  16354  pospo  18278  mgm2nsgrplem2  18856  eqg0subg  19137  rhmdvdsr  20453  lsmcv  21108  sraring  21150  opsrtoslem1  22022  madugsum  22599  hauscmplem  23362  bwth  23366  ptbasfi  23537  hmphindis  23753  fbncp  23795  fgcl  23834  fixufil  23878  uffixfr  23879  mbfima  25599  mbfimaicc  25600  ig1pdvds  26153  zabsle1  27275  tgldimor  28586  ax5seglem4  29017  axcontlem2  29050  axcontlem4  29052  nbgrval  29421  cusgrfi  29544  fusgrregdegfi  29655  rusgr1vtxlem  29673  wlkiswwlksupgr2  29962  elwwlks2ons3  30040  clwwlknonwwlknonb  30193  eucrctshift  30330  spansncvi  31740  eigposi  31924  pjnormssi  32256  sumdmdlem  32506  tngdim  33791  bnj168  34907  bnj964  35119  bnj966  35120  bnj1398  35210  fnrelpredd  35268  lfuhgr3  35336  acycgrislfgr  35368  cgrdegen  36220  btwnconn1lem11  36313  btwnconn1lem12  36314  btwnconn1lem14  36316  bj-opelidb1  37408  bj-inexeqex  37409  bj-idreseqb  37418  bj-ideqg1ALT  37420  bj-ccinftydisj  37468  phpreu  37855  fin2so  37858  matunitlindflem2  37868  poimirlem26  37897  poimirlem28  37899  dvasin  37955  isbnd2  38034  atcvrj0  39804  paddasslem5  40200  expeq1d  42694  pm13.13a  44763  iotavalb  44786  suctrALTcf  45277  suctrALTcfVD  45278  suctrALT3  45279  unisnALT  45281  2sb5ndALT  45287  xreqle  45679  supminfxr2  45827  fourierdlem40  46505  fourierdlem78  46542  tz6.12-afv2  47600  afv2fv0  47625  2ffzoeq  47687  clnbgrval  48182  dfsclnbgr6  48218  uspgrlimlem1  48348  uspgropssxp  48504  uspgrsprfo  48508  nn0sumshdiglemA  48979  itscnhlc0yqe  49119