Theorem biimpac 484

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  r19.29r  3130  gencbvex2  3511  2reu5  3719  sseq0  4357  ifpprsnss  4727  dfiun2g  4993  poltletr  6144  ordnbtwn  6484  funopsn  7183  funopsnOLD  7184  onsucuni2  7879  1stconst  8148  2ndconst  8149  smo11  8410  omlimcl  8624  omxpenlem  9135  fodomr  9185  f1oenfirn  9233  f1domfi  9234  fodomfib  9358  infsupprpr  9535  r1val1  9830  alephval3  10228  dfac5lem4  10244  dfac5  10246  axdc4lem  10572  fodomb  10644  distrlem1pr  11149  map2psrpr  11234  supsrlem  11235  eqle  11451  swrd0  14850  repswswrd  14977  cshwidxmod  14996  rtrclind  15261  sumz  15932  prod1  16155  divalglem8  16614  flodddiv4  16629  pospo  18567  mgm2nsgrplem2  19168  eqg0subg  19461  rhmdvdsr  20809  lsmcv  21470  sraring  21512  opsrtoslem1  22419  madugsum  23013  matunitlindflem2  23050  hauscmplem  23779  bwth  23783  ptbasfi  23955  hmphindis  24171  fbncp  24213  fgcl  24252  fixufil  24296  uffixfr  24297  mbfima  26006  mbfimaicc  26007  ig1pdvds  26553  zabsle1  27680  tgldimor  29022  ax5seglem4  29567  axcontlem2  29600  axcontlem4  29602  lfuhgr3  29785  nbgrval  29974  cusgrfi  30096  fusgrregdegfi  30207  rusgr1vtxlem  30225  wlkiswwlksupgr2  30523  elwwlks2ons3  30601  clwwlknonwwlknonb  30754  eucrctshift  30901  spansncvi  32311  eigposi  32495  pjnormssi  32827  sumdmdlem  33077  tngdim  34356  bnj168  35472  bnj964  35684  bnj966  35685  bnj1398  35775  fnrelpredd  35845  acwer1prc  35893  acycgrislfgr  36115  cgrdegen  36984  btwnconn1lem11  37077  btwnconn1lem12  37078  btwnconn1lem14  37080  bj-opelidb1  38342  bj-inexeqex  38343  bj-idreseqb  38352  bj-ideqg1ALT  38354  bj-ccinftydisj  38402  phpreu  38795  fin2so  38798  poimirlem26  38832  poimirlem28  38834  dvasin  38890  isbnd2  38983  atcvrj0  40751  paddasslem5  41147  expeq1d  43647  pm13.13a  45652  iotavalb  45674  suctrALTcf  46164  suctrALTcfVD  46165  suctrALT3  46166  unisnALT  46168  2sb5ndALT  46174  xreqle  46605  supminfxr2  46752  fourierdlem40  47430  fourierdlem78  47467  tz6.12-afv2  48583  afv2fv0  48608  2ffzoeq  48671  clnbgrval  49193  dfsclnbgr6  49229  uspgrlimlem1  49359  uspgropssxp  49515  uspgrsprfo  49519  nn0sumshdiglemA  50062  itscnhlc0yqe  50202