Theorem biimpac 472

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  gencbvex2  3453  2reu5  3633  ifpprsnss  4531  poltletr  5785  ordnbtwn  6068  tz6.12-1  6470  funopsn  6681  onsucuni2  7314  1stconst  7548  2ndconst  7549  smo11  7746  omlimcl  7944  omxpenlem  8351  fodomr  8401  fodomfib  8530  infsupprpr  8700  r1val1  8948  alephval3  9268  dfac5lem4  9284  dfac5  9286  axdc4lem  9614  fodomb  9685  distrlem1pr  10184  map2psrpr  10269  supsrlem  10270  eqle  10480  ccat1st1st  13722  swrd0  13757  reuccats1lemOLD  13851  repswswrd  13934  cshwidxmod  13958  rtrclind  14216  sumz  14864  prod1  15081  divalglem8  15534  flodddiv4  15547  pospo  17363  mgm2nsgrplem2  17797  lsmcv  19541  opsrtoslem1  19884  psrbagfsupp  19909  madugsum  20858  hauscmplem  21622  bwth  21626  ptbasfi  21797  hmphindis  22013  fbncp  22055  fgcl  22094  fixufil  22138  uffixfr  22139  mbfima  23838  mbfimaicc  23839  ig1pdvds  24377  zabsle1  25477  tgldimor  25857  ax5seglem4  26285  axcontlem2  26318  axcontlem4  26320  nbgrval  26687  cusgrfi  26810  fusgrregdegfi  26921  rusgr1vtxlem  26939  wlkiswwlksupgr2  27230  elwwlks2ons3  27339  clwwlknonwwlknonb  27512  eucrctshift  27651  spansncvi  29087  eigposi  29271  pjnormssi  29603  sumdmdlem  29853  rhmdvdsr  30384  tngdim  30432  bnj168  31402  bnj521  31409  bnj964  31616  bnj966  31617  bnj1398  31705  cgrdegen  32704  btwnconn1lem11  32797  btwnconn1lem12  32798  btwnconn1lem14  32800  bj-elid3  33669  bj-ccinftydisj  33694  cnfinltrel  33839  phpreu  34023  fin2so  34026  matunitlindflem2  34037  poimirlem26  34066  poimirlem28  34068  dvasin  34126  isbnd2  34211  atcvrj0  35587  paddasslem5  35983  pm13.13a  39573  iotavalb  39596  suctrALTcf  40101  suctrALTcfVD  40102  suctrALT3  40103  unisnALT  40105  2sb5ndALT  40111  xreqle  40452  supminfxr2  40614  fourierdlem40  41301  fourierdlem78  41338  tz6.12-afv2  42291  afv2fv0  42316  2ffzoeq  42380  uspgropssxp  42777  uspgrsprfo  42781  difmodm1lt  43342  nn0sumshdiglemA  43438  itscnhlc0yqe  43505