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  3102  gencbvex2  3489  2reu5  3705  ifpprsnss  4709  dfiun2g  4973  poltletr  6090  ordnbtwn  6413  funopsn  7096  onsucuni2  7779  1stconst  8044  2ndconst  8045  smo11  8298  omlimcl  8507  omxpenlem  9010  fodomr  9060  f1oenfirn  9108  f1domfi  9109  fodomfib  9233  fodomfibOLD  9235  infsupprpr  9413  r1val1  9704  alephval3  10026  dfac5lem4  10042  dfac5lem4OLD  10044  dfac5  10045  axdc4lem  10371  fodomb  10442  distrlem1pr  10942  map2psrpr  11027  supsrlem  11028  eqle  11242  swrd0  14615  repswswrd  14740  cshwidxmod  14759  rtrclind  15021  sumz  15678  prod1  15903  divalglem8  16363  flodddiv4  16378  pospo  18303  mgm2nsgrplem2  18884  eqg0subg  19165  rhmdvdsr  20479  lsmcv  21134  sraring  21176  opsrtoslem1  22046  madugsum  22621  hauscmplem  23384  bwth  23388  ptbasfi  23559  hmphindis  23775  fbncp  23817  fgcl  23856  fixufil  23900  uffixfr  23901  mbfima  25610  mbfimaicc  25611  ig1pdvds  26158  zabsle1  27276  tgldimor  28587  ax5seglem4  29018  axcontlem2  29051  axcontlem4  29053  nbgrval  29422  cusgrfi  29545  fusgrregdegfi  29656  rusgr1vtxlem  29674  wlkiswwlksupgr2  29963  elwwlks2ons3  30041  clwwlknonwwlknonb  30194  eucrctshift  30331  spansncvi  31741  eigposi  31925  pjnormssi  32257  sumdmdlem  32507  tngdim  33776  bnj168  34892  bnj964  35104  bnj966  35105  bnj1398  35195  fnrelpredd  35253  lfuhgr3  35321  acycgrislfgr  35353  cgrdegen  36205  btwnconn1lem11  36298  btwnconn1lem12  36299  btwnconn1lem14  36301  bj-opelidb1  37486  bj-inexeqex  37487  bj-idreseqb  37496  bj-ideqg1ALT  37498  bj-ccinftydisj  37546  phpreu  37942  fin2so  37945  matunitlindflem2  37955  poimirlem26  37984  poimirlem28  37986  dvasin  38042  isbnd2  38121  atcvrj0  39891  paddasslem5  40287  expeq1d  42773  pm13.13a  44855  iotavalb  44878  suctrALTcf  45369  suctrALTcfVD  45370  suctrALT3  45371  unisnALT  45373  2sb5ndALT  45379  xreqle  45771  supminfxr2  45918  fourierdlem40  46596  fourierdlem78  46633  tz6.12-afv2  47703  afv2fv0  47728  2ffzoeq  47791  clnbgrval  48313  dfsclnbgr6  48349  uspgrlimlem1  48479  uspgropssxp  48635  uspgrsprfo  48639  nn0sumshdiglemA  49110  itscnhlc0yqe  49250