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  3486  2reu5  3692  ifpprsnss  4700  poltletr  6030  ordnbtwn  6349  tz6.12-1  6788  funopsn  7012  onsucuni2  7671  1stconst  7927  2ndconst  7928  smo11  8182  omlimcl  8396  omxpenlem  8847  fodomr  8902  f1oenfirn  8953  f1domfi  8954  fodomfib  9080  infsupprpr  9250  r1val1  9554  alephval3  9876  dfac5lem4  9892  dfac5  9894  axdc4lem  10221  fodomb  10292  distrlem1pr  10791  map2psrpr  10876  supsrlem  10877  eqle  11087  swrd0  14381  repswswrd  14507  cshwidxmod  14526  rtrclind  14786  sumz  15444  prod1  15664  divalglem8  16119  flodddiv4  16132  pospo  18073  mgm2nsgrplem2  18568  lsmcv  20413  psrbagfsuppOLD  21134  opsrtoslem1  21272  madugsum  21802  hauscmplem  22567  bwth  22571  ptbasfi  22742  hmphindis  22958  fbncp  23000  fgcl  23039  fixufil  23083  uffixfr  23084  mbfima  24804  mbfimaicc  24805  ig1pdvds  25351  zabsle1  26454  tgldimor  26873  ax5seglem4  27310  axcontlem2  27343  axcontlem4  27345  nbgrval  27713  cusgrfi  27835  fusgrregdegfi  27946  rusgr1vtxlem  27964  wlkiswwlksupgr2  28250  elwwlks2ons3  28328  clwwlknonwwlknonb  28478  eucrctshift  28615  spansncvi  30022  eigposi  30206  pjnormssi  30538  sumdmdlem  30788  rhmdvdsr  31525  sraring  31680  tngdim  31704  bnj168  32717  bnj521  32724  bnj964  32931  bnj966  32932  bnj1398  33022  fnrelpredd  33069  lfuhgr3  33089  acycgrislfgr  33122  cgrdegen  34314  btwnconn1lem11  34407  btwnconn1lem12  34408  btwnconn1lem14  34410  bj-opelidb1  35332  bj-inexeqex  35333  bj-idreseqb  35342  bj-ideqg1ALT  35344  bj-ccinftydisj  35392  phpreu  35769  fin2so  35772  matunitlindflem2  35782  poimirlem26  35811  poimirlem28  35813  dvasin  35869  isbnd2  35949  atcvrj0  37450  paddasslem5  37846  pm13.13a  42006  iotavalb  42029  suctrALTcf  42523  suctrALTcfVD  42524  suctrALT3  42525  unisnALT  42527  2sb5ndALT  42533  xreqle  42838  supminfxr2  42990  fourierdlem40  43669  fourierdlem78  43706  tz6.12-afv2  44710  afv2fv0  44735  2ffzoeq  44798  uspgropssxp  45284  uspgrsprfo  45288  difmodm1lt  45846  nn0sumshdiglemA  45943  itscnhlc0yqe  46083