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  3101  gencbvex2  3488  2reu5  3704  ifpprsnss  4708  dfiun2g  4972  poltletr  6095  ordnbtwn  6418  funopsn  7101  funopsnOLD  7102  onsucuni2  7785  1stconst  8050  2ndconst  8051  smo11  8304  omlimcl  8513  omxpenlem  9016  fodomr  9066  f1oenfirn  9114  f1domfi  9115  fodomfib  9239  fodomfibOLD  9241  infsupprpr  9419  r1val1  9710  alephval3  10032  dfac5lem4  10048  dfac5lem4OLD  10050  dfac5  10051  axdc4lem  10377  fodomb  10448  distrlem1pr  10948  map2psrpr  11033  supsrlem  11034  eqle  11248  swrd0  14621  repswswrd  14746  cshwidxmod  14765  rtrclind  15027  sumz  15684  prod1  15909  divalglem8  16369  flodddiv4  16384  pospo  18309  mgm2nsgrplem2  18890  eqg0subg  19171  rhmdvdsr  20485  lsmcv  21139  sraring  21181  opsrtoslem1  22033  madugsum  22608  hauscmplem  23371  bwth  23375  ptbasfi  23546  hmphindis  23762  fbncp  23804  fgcl  23843  fixufil  23887  uffixfr  23888  mbfima  25597  mbfimaicc  25598  ig1pdvds  26145  zabsle1  27259  tgldimor  28570  ax5seglem4  29001  axcontlem2  29034  axcontlem4  29036  nbgrval  29405  cusgrfi  29527  fusgrregdegfi  29638  rusgr1vtxlem  29656  wlkiswwlksupgr2  29945  elwwlks2ons3  30023  clwwlknonwwlknonb  30176  eucrctshift  30313  spansncvi  31723  eigposi  31907  pjnormssi  32239  sumdmdlem  32489  tngdim  33757  bnj168  34873  bnj964  35085  bnj966  35086  bnj1398  35176  fnrelpredd  35234  lfuhgr3  35302  acycgrislfgr  35334  cgrdegen  36186  btwnconn1lem11  36279  btwnconn1lem12  36280  btwnconn1lem14  36282  bj-opelidb1  37467  bj-inexeqex  37468  bj-idreseqb  37477  bj-ideqg1ALT  37479  bj-ccinftydisj  37527  phpreu  37925  fin2so  37928  matunitlindflem2  37938  poimirlem26  37967  poimirlem28  37969  dvasin  38025  isbnd2  38104  atcvrj0  39874  paddasslem5  40270  expeq1d  42756  pm13.13a  44834  iotavalb  44857  suctrALTcf  45348  suctrALTcfVD  45349  suctrALT3  45350  unisnALT  45352  2sb5ndALT  45358  xreqle  45750  supminfxr2  45897  fourierdlem40  46575  fourierdlem78  46612  tz6.12-afv2  47688  afv2fv0  47713  2ffzoeq  47776  clnbgrval  48298  dfsclnbgr6  48334  uspgrlimlem1  48464  uspgropssxp  48620  uspgrsprfo  48624  nn0sumshdiglemA  49095  itscnhlc0yqe  49235