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:  gencbvex2  3489  2reu5  3693  ifpprsnss  4700  dfiun2g  4960  poltletr  6037  ordnbtwn  6356  tz6.12-1  6796  funopsn  7020  onsucuni2  7681  1stconst  7940  2ndconst  7941  smo11  8195  omlimcl  8409  omxpenlem  8860  fodomr  8915  f1oenfirn  8966  f1domfi  8967  fodomfib  9093  infsupprpr  9263  r1val1  9544  alephval3  9866  dfac5lem4  9882  dfac5  9884  axdc4lem  10211  fodomb  10282  distrlem1pr  10781  map2psrpr  10866  supsrlem  10867  eqle  11077  swrd0  14371  repswswrd  14497  cshwidxmod  14516  rtrclind  14776  sumz  15434  prod1  15654  divalglem8  16109  flodddiv4  16122  pospo  18063  mgm2nsgrplem2  18558  lsmcv  20403  psrbagfsuppOLD  21124  opsrtoslem1  21262  madugsum  21792  hauscmplem  22557  bwth  22561  ptbasfi  22732  hmphindis  22948  fbncp  22990  fgcl  23029  fixufil  23073  uffixfr  23074  mbfima  24794  mbfimaicc  24795  ig1pdvds  25341  zabsle1  26444  tgldimor  26863  ax5seglem4  27300  axcontlem2  27333  axcontlem4  27335  nbgrval  27703  cusgrfi  27825  fusgrregdegfi  27936  rusgr1vtxlem  27954  wlkiswwlksupgr2  28242  elwwlks2ons3  28320  clwwlknonwwlknonb  28470  eucrctshift  28607  spansncvi  30014  eigposi  30198  pjnormssi  30530  sumdmdlem  30780  rhmdvdsr  31517  sraring  31672  tngdim  31696  bnj168  32709  bnj521  32716  bnj964  32923  bnj966  32924  bnj1398  33014  fnrelpredd  33061  lfuhgr3  33081  acycgrislfgr  33114  cgrdegen  34306  btwnconn1lem11  34399  btwnconn1lem12  34400  btwnconn1lem14  34402  bj-opelidb1  35324  bj-inexeqex  35325  bj-idreseqb  35334  bj-ideqg1ALT  35336  bj-ccinftydisj  35384  phpreu  35761  fin2so  35764  matunitlindflem2  35774  poimirlem26  35803  poimirlem28  35805  dvasin  35861  isbnd2  35941  atcvrj0  37442  paddasslem5  37838  pm13.13a  42025  iotavalb  42048  suctrALTcf  42542  suctrALTcfVD  42543  suctrALT3  42544  unisnALT  42546  2sb5ndALT  42552  xreqle  42857  supminfxr2  43009  fourierdlem40  43688  fourierdlem78  43725  tz6.12-afv2  44732  afv2fv0  44757  2ffzoeq  44820  uspgropssxp  45306  uspgrsprfo  45310  difmodm1lt  45868  nn0sumshdiglemA  45965  itscnhlc0yqe  46105