Theorem biimpac 478

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  r19.29r  3096  gencbvex2  3505  2reu5  3726  ifpprsnss  4724  dfiun2g  4990  poltletr  6093  ordnbtwn  6415  tz6.12-1OLD  6864  funopsn  7102  onsucuni2  7789  1stconst  8056  2ndconst  8057  smo11  8310  omlimcl  8519  omxpenlem  9019  fodomr  9069  f1oenfirn  9121  f1domfi  9122  fodomfib  9256  fodomfibOLD  9258  infsupprpr  9433  r1val1  9715  alephval3  10039  dfac5lem4  10055  dfac5lem4OLD  10057  dfac5  10058  axdc4lem  10384  fodomb  10455  distrlem1pr  10954  map2psrpr  11039  supsrlem  11040  eqle  11252  swrd0  14599  repswswrd  14725  cshwidxmod  14744  rtrclind  15007  sumz  15664  prod1  15886  divalglem8  16346  flodddiv4  16361  pospo  18284  mgm2nsgrplem2  18828  eqg0subg  19110  rhmdvdsr  20428  lsmcv  21083  sraring  21125  opsrtoslem1  21995  madugsum  22563  hauscmplem  23326  bwth  23330  ptbasfi  23501  hmphindis  23717  fbncp  23759  fgcl  23798  fixufil  23842  uffixfr  23843  mbfima  25564  mbfimaicc  25565  ig1pdvds  26118  zabsle1  27240  tgldimor  28482  ax5seglem4  28912  axcontlem2  28945  axcontlem4  28947  nbgrval  29316  cusgrfi  29439  fusgrregdegfi  29550  rusgr1vtxlem  29568  wlkiswwlksupgr2  29857  elwwlks2ons3  29935  clwwlknonwwlknonb  30085  eucrctshift  30222  spansncvi  31631  eigposi  31815  pjnormssi  32147  sumdmdlem  32397  tngdim  33602  bnj168  34713  bnj964  34926  bnj966  34927  bnj1398  35017  fnrelpredd  35072  lfuhgr3  35100  acycgrislfgr  35132  cgrdegen  35985  btwnconn1lem11  36078  btwnconn1lem12  36079  btwnconn1lem14  36081  bj-opelidb1  37134  bj-inexeqex  37135  bj-idreseqb  37144  bj-ideqg1ALT  37146  bj-ccinftydisj  37194  phpreu  37591  fin2so  37594  matunitlindflem2  37604  poimirlem26  37633  poimirlem28  37635  dvasin  37691  isbnd2  37770  atcvrj0  39415  paddasslem5  39811  expeq1d  42305  pm13.13a  44389  iotavalb  44412  suctrALTcf  44904  suctrALTcfVD  44905  suctrALT3  44906  unisnALT  44908  2sb5ndALT  44914  xreqle  45308  supminfxr2  45458  fourierdlem40  46138  fourierdlem78  46175  tz6.12-afv2  47234  afv2fv0  47259  2ffzoeq  47321  clnbgrval  47816  dfsclnbgr6  47851  uspgrlimlem1  47980  uspgropssxp  48125  uspgrsprfo  48129  nn0sumshdiglemA  48601  itscnhlc0yqe  48741