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  3098  gencbvex2  3498  2reu5  3714  ifpprsnss  4719  dfiun2g  4983  poltletr  6087  ordnbtwn  6410  funopsn  7091  onsucuni2  7774  1stconst  8040  2ndconst  8041  smo11  8294  omlimcl  8503  omxpenlem  9004  fodomr  9054  f1oenfirn  9102  f1domfi  9103  fodomfib  9227  fodomfibOLD  9229  infsupprpr  9407  r1val1  9696  alephval3  10018  dfac5lem4  10034  dfac5lem4OLD  10036  dfac5  10037  axdc4lem  10363  fodomb  10434  distrlem1pr  10934  map2psrpr  11019  supsrlem  11020  eqle  11233  swrd0  14580  repswswrd  14705  cshwidxmod  14724  rtrclind  14986  sumz  15643  prod1  15865  divalglem8  16325  flodddiv4  16340  pospo  18264  mgm2nsgrplem2  18842  eqg0subg  19123  rhmdvdsr  20439  lsmcv  21094  sraring  21136  opsrtoslem1  22008  madugsum  22585  hauscmplem  23348  bwth  23352  ptbasfi  23523  hmphindis  23739  fbncp  23781  fgcl  23820  fixufil  23864  uffixfr  23865  mbfima  25585  mbfimaicc  25586  ig1pdvds  26139  zabsle1  27261  tgldimor  28523  ax5seglem4  28954  axcontlem2  28987  axcontlem4  28989  nbgrval  29358  cusgrfi  29481  fusgrregdegfi  29592  rusgr1vtxlem  29610  wlkiswwlksupgr2  29899  elwwlks2ons3  29977  clwwlknonwwlknonb  30130  eucrctshift  30267  spansncvi  31676  eigposi  31860  pjnormssi  32192  sumdmdlem  32442  tngdim  33719  bnj168  34835  bnj964  35048  bnj966  35049  bnj1398  35139  fnrelpredd  35196  lfuhgr3  35263  acycgrislfgr  35295  cgrdegen  36147  btwnconn1lem11  36240  btwnconn1lem12  36241  btwnconn1lem14  36243  bj-opelidb1  37297  bj-inexeqex  37298  bj-idreseqb  37307  bj-ideqg1ALT  37309  bj-ccinftydisj  37357  phpreu  37744  fin2so  37747  matunitlindflem2  37757  poimirlem26  37786  poimirlem28  37788  dvasin  37844  isbnd2  37923  atcvrj0  39627  paddasslem5  40023  expeq1d  42521  pm13.13a  44590  iotavalb  44613  suctrALTcf  45104  suctrALTcfVD  45105  suctrALT3  45106  unisnALT  45108  2sb5ndALT  45114  xreqle  45507  supminfxr2  45655  fourierdlem40  46333  fourierdlem78  46370  tz6.12-afv2  47428  afv2fv0  47453  2ffzoeq  47515  clnbgrval  48010  dfsclnbgr6  48046  uspgrlimlem1  48176  uspgropssxp  48332  uspgrsprfo  48336  nn0sumshdiglemA  48807  itscnhlc0yqe  48947