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  3100  gencbvex2  3500  2reu5  3716  ifpprsnss  4721  dfiun2g  4985  poltletr  6089  ordnbtwn  6412  funopsn  7093  onsucuni2  7776  1stconst  8042  2ndconst  8043  smo11  8296  omlimcl  8505  omxpenlem  9006  fodomr  9056  f1oenfirn  9104  f1domfi  9105  fodomfib  9229  fodomfibOLD  9231  infsupprpr  9409  r1val1  9698  alephval3  10020  dfac5lem4  10036  dfac5lem4OLD  10038  dfac5  10039  axdc4lem  10365  fodomb  10436  distrlem1pr  10936  map2psrpr  11021  supsrlem  11022  eqle  11235  swrd0  14582  repswswrd  14707  cshwidxmod  14726  rtrclind  14988  sumz  15645  prod1  15867  divalglem8  16327  flodddiv4  16342  pospo  18266  mgm2nsgrplem2  18844  eqg0subg  19125  rhmdvdsr  20441  lsmcv  21096  sraring  21138  opsrtoslem1  22010  madugsum  22587  hauscmplem  23350  bwth  23354  ptbasfi  23525  hmphindis  23741  fbncp  23783  fgcl  23822  fixufil  23866  uffixfr  23867  mbfima  25587  mbfimaicc  25588  ig1pdvds  26141  zabsle1  27263  tgldimor  28574  ax5seglem4  29005  axcontlem2  29038  axcontlem4  29040  nbgrval  29409  cusgrfi  29532  fusgrregdegfi  29643  rusgr1vtxlem  29661  wlkiswwlksupgr2  29950  elwwlks2ons3  30028  clwwlknonwwlknonb  30181  eucrctshift  30318  spansncvi  31727  eigposi  31911  pjnormssi  32243  sumdmdlem  32493  tngdim  33770  bnj168  34886  bnj964  35099  bnj966  35100  bnj1398  35190  fnrelpredd  35247  lfuhgr3  35314  acycgrislfgr  35346  cgrdegen  36198  btwnconn1lem11  36291  btwnconn1lem12  36292  btwnconn1lem14  36294  bj-opelidb1  37358  bj-inexeqex  37359  bj-idreseqb  37368  bj-ideqg1ALT  37370  bj-ccinftydisj  37418  phpreu  37805  fin2so  37808  matunitlindflem2  37818  poimirlem26  37847  poimirlem28  37849  dvasin  37905  isbnd2  37984  atcvrj0  39698  paddasslem5  40094  expeq1d  42589  pm13.13a  44658  iotavalb  44681  suctrALTcf  45172  suctrALTcfVD  45173  suctrALT3  45174  unisnALT  45176  2sb5ndALT  45182  xreqle  45575  supminfxr2  45723  fourierdlem40  46401  fourierdlem78  46438  tz6.12-afv2  47496  afv2fv0  47521  2ffzoeq  47583  clnbgrval  48078  dfsclnbgr6  48114  uspgrlimlem1  48244  uspgropssxp  48400  uspgrsprfo  48404  nn0sumshdiglemA  48875  itscnhlc0yqe  49015