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  3113  gencbvex2  3541  2reu5  3766  ifpprsnss  4768  dfiun2g  5034  poltletr  6154  ordnbtwn  6478  tz6.12-1OLD  6930  funopsn  7167  onsucuni2  7853  1stconst  8123  2ndconst  8124  smo11  8402  omlimcl  8614  omxpenlem  9111  fodomr  9166  f1oenfirn  9217  f1domfi  9218  fodomfib  9366  fodomfibOLD  9368  infsupprpr  9541  r1val1  9823  alephval3  10147  dfac5lem4  10163  dfac5lem4OLD  10165  dfac5  10166  axdc4lem  10492  fodomb  10563  distrlem1pr  11062  map2psrpr  11147  supsrlem  11148  eqle  11360  swrd0  14692  repswswrd  14818  cshwidxmod  14837  rtrclind  15100  sumz  15754  prod1  15976  divalglem8  16433  flodddiv4  16448  pospo  18402  mgm2nsgrplem2  18944  eqg0subg  19226  rhmdvdsr  20524  lsmcv  21160  sraring  21210  opsrtoslem1  22096  madugsum  22664  hauscmplem  23429  bwth  23433  ptbasfi  23604  hmphindis  23820  fbncp  23862  fgcl  23901  fixufil  23945  uffixfr  23946  mbfima  25678  mbfimaicc  25679  ig1pdvds  26233  zabsle1  27354  tgldimor  28524  ax5seglem4  28961  axcontlem2  28994  axcontlem4  28996  nbgrval  29367  cusgrfi  29490  fusgrregdegfi  29601  rusgr1vtxlem  29619  wlkiswwlksupgr2  29906  elwwlks2ons3  29984  clwwlknonwwlknonb  30134  eucrctshift  30271  spansncvi  31680  eigposi  31864  pjnormssi  32196  sumdmdlem  32446  tngdim  33640  bnj168  34722  bnj964  34935  bnj966  34936  bnj1398  35026  fnrelpredd  35081  lfuhgr3  35103  acycgrislfgr  35136  cgrdegen  35985  btwnconn1lem11  36078  btwnconn1lem12  36079  btwnconn1lem14  36081  bj-opelidb1  37135  bj-inexeqex  37136  bj-idreseqb  37145  bj-ideqg1ALT  37147  bj-ccinftydisj  37195  phpreu  37590  fin2so  37593  matunitlindflem2  37603  poimirlem26  37632  poimirlem28  37634  dvasin  37690  isbnd2  37769  atcvrj0  39410  paddasslem5  39806  expeq1d  42337  pm13.13a  44402  iotavalb  44425  suctrALTcf  44919  suctrALTcfVD  44920  suctrALT3  44921  unisnALT  44923  2sb5ndALT  44929  xreqle  45268  supminfxr2  45418  fourierdlem40  46102  fourierdlem78  46139  tz6.12-afv2  47189  afv2fv0  47214  2ffzoeq  47276  clnbgrval  47746  dfsclnbgr6  47781  uspgrlimlem1  47890  uspgropssxp  47987  uspgrsprfo  47991  difmodm1lt  48371  nn0sumshdiglemA  48468  itscnhlc0yqe  48608