Theorem biimpac 482

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  gencbvex2  3498  2reu5  3697  ifpprsnss  4660  poltletr  5959  ordnbtwn  6249  tz6.12-1  6667  funopsn  6887  onsucuni2  7529  1stconst  7778  2ndconst  7779  smo11  7984  omlimcl  8187  omxpenlem  8601  fodomr  8652  fodomfib  8782  infsupprpr  8952  r1val1  9199  alephval3  9521  dfac5lem4  9537  dfac5  9539  axdc4lem  9866  fodomb  9937  distrlem1pr  10436  map2psrpr  10521  supsrlem  10522  eqle  10731  swrd0  14011  repswswrd  14137  cshwidxmod  14156  rtrclind  14416  sumz  15071  prod1  15290  divalglem8  15741  flodddiv4  15754  pospo  17575  mgm2nsgrplem2  18076  lsmcv  19906  opsrtoslem1  20723  psrbagfsupp  20748  madugsum  21248  hauscmplem  22011  bwth  22015  ptbasfi  22186  hmphindis  22402  fbncp  22444  fgcl  22483  fixufil  22527  uffixfr  22528  mbfima  24234  mbfimaicc  24235  ig1pdvds  24777  zabsle1  25880  tgldimor  26296  ax5seglem4  26726  axcontlem2  26759  axcontlem4  26761  nbgrval  27126  cusgrfi  27248  fusgrregdegfi  27359  rusgr1vtxlem  27377  wlkiswwlksupgr2  27663  elwwlks2ons3  27741  clwwlknonwwlknonb  27891  eucrctshift  28028  spansncvi  29435  eigposi  29619  pjnormssi  29951  sumdmdlem  30201  rhmdvdsr  30942  sraring  31075  tngdim  31099  bnj168  32110  bnj521  32117  bnj964  32325  bnj966  32326  bnj1398  32416  fnrelpredd  32472  lfuhgr3  32479  acycgrislfgr  32512  cgrdegen  33578  btwnconn1lem11  33671  btwnconn1lem12  33672  btwnconn1lem14  33674  bj-opelidb1  34568  bj-inexeqex  34569  bj-idreseqb  34578  bj-ideqg1ALT  34580  bj-ccinftydisj  34628  phpreu  35041  fin2so  35044  matunitlindflem2  35054  poimirlem26  35083  poimirlem28  35085  dvasin  35141  isbnd2  35221  atcvrj0  36724  paddasslem5  37120  pm13.13a  41111  iotavalb  41134  suctrALTcf  41628  suctrALTcfVD  41629  suctrALT3  41630  unisnALT  41632  2sb5ndALT  41638  xreqle  41950  supminfxr2  42108  fourierdlem40  42789  fourierdlem78  42826  tz6.12-afv2  43796  afv2fv0  43821  2ffzoeq  43885  uspgropssxp  44372  uspgrsprfo  44376  difmodm1lt  44936  nn0sumshdiglemA  45033  itscnhlc0yqe  45173