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

Syntax hints:   → wi 4   ↔ wb 208   ∧ 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 209  df-an 400

This theorem is referenced by:  r19.29r  3126  gencbvex2  3511  2reu5  3721  ifpprsnss  4723  dfiun2g  4987  poltletr  6119  ordnbtwn  6441  funopsn  7130  funopsnOLD  7131  onsucuni2  7814  1stconst  8079  2ndconst  8080  smo11  8335  omlimcl  8547  omxpenlem  9050  fodomr  9100  f1oenfirn  9148  f1domfi  9149  fodomfib  9273  fodomfibOLD  9274  infsupprpr  9452  r1val1  9744  alephval3  10066  dfac5lem4  10082  dfac5lem4OLD  10084  dfac5  10085  axdc4lem  10412  fodomb  10483  distrlem1pr  10983  map2psrpr  11068  supsrlem  11069  eqle  11285  swrd0  14672  repswswrd  14797  cshwidxmod  14816  rtrclind  15078  sumz  15749  prod1  15974  divalglem8  16434  flodddiv4  16449  pospo  18375  mgm2nsgrplem2  18956  eqg0subg  19237  rhmdvdsr  20558  lsmcv  21211  sraring  21253  opsrtoslem1  22108  madugsum  22703  hauscmplem  23466  bwth  23470  ptbasfi  23641  hmphindis  23857  fbncp  23899  fgcl  23938  fixufil  23982  uffixfr  23983  mbfima  25692  mbfimaicc  25693  ig1pdvds  26240  zabsle1  27360  tgldimor  28671  ax5seglem4  29133  axcontlem2  29166  axcontlem4  29168  nbgrval  29537  cusgrfi  29659  fusgrregdegfi  29770  rusgr1vtxlem  29788  wlkiswwlksupgr2  30077  elwwlks2ons3  30155  clwwlknonwwlknonb  30308  eucrctshift  30445  spansncvi  31855  eigposi  32039  pjnormssi  32371  sumdmdlem  32621  tngdim  33910  bnj168  35026  bnj964  35238  bnj966  35239  bnj1398  35329  fnrelpredd  35387  lfuhgr3  35470  acycgrislfgr  35502  cgrdegen  36354  btwnconn1lem11  36447  btwnconn1lem12  36448  btwnconn1lem14  36450  bj-opelidb1  37645  bj-inexeqex  37646  bj-idreseqb  37655  bj-ideqg1ALT  37657  bj-ccinftydisj  37705  phpreu  38103  fin2so  38106  matunitlindflem2  38116  poimirlem26  38145  poimirlem28  38147  dvasin  38203  isbnd2  38282  atcvrj0  40052  paddasslem5  40448  expeq1d  42933  pm13.13a  44983  iotavalb  45006  suctrALTcf  45497  suctrALTcfVD  45498  suctrALT3  45499  unisnALT  45501  2sb5ndALT  45507  xreqle  45896  supminfxr2  46043  fourierdlem40  46721  fourierdlem78  46758  tz6.12-afv2  47834  afv2fv0  47859  2ffzoeq  47922  clnbgrval  48444  dfsclnbgr6  48480  uspgrlimlem1  48610  uspgropssxp  48766  uspgrsprfo  48770  nn0sumshdiglemA  49241  itscnhlc0yqe  49381