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  3097  gencbvex2  3511  2reu5  3732  ifpprsnss  4731  dfiun2g  4997  poltletr  6108  ordnbtwn  6430  tz6.12-1OLD  6885  funopsn  7123  onsucuni2  7812  1stconst  8082  2ndconst  8083  smo11  8336  omlimcl  8545  omxpenlem  9047  fodomr  9098  f1oenfirn  9150  f1domfi  9151  fodomfib  9287  fodomfibOLD  9289  infsupprpr  9464  r1val1  9746  alephval3  10070  dfac5lem4  10086  dfac5lem4OLD  10088  dfac5  10089  axdc4lem  10415  fodomb  10486  distrlem1pr  10985  map2psrpr  11070  supsrlem  11071  eqle  11283  swrd0  14630  repswswrd  14756  cshwidxmod  14775  rtrclind  15038  sumz  15695  prod1  15917  divalglem8  16377  flodddiv4  16392  pospo  18311  mgm2nsgrplem2  18853  eqg0subg  19135  rhmdvdsr  20424  lsmcv  21058  sraring  21100  opsrtoslem1  21969  madugsum  22537  hauscmplem  23300  bwth  23304  ptbasfi  23475  hmphindis  23691  fbncp  23733  fgcl  23772  fixufil  23816  uffixfr  23817  mbfima  25538  mbfimaicc  25539  ig1pdvds  26092  zabsle1  27214  tgldimor  28436  ax5seglem4  28866  axcontlem2  28899  axcontlem4  28901  nbgrval  29270  cusgrfi  29393  fusgrregdegfi  29504  rusgr1vtxlem  29522  wlkiswwlksupgr2  29814  elwwlks2ons3  29892  clwwlknonwwlknonb  30042  eucrctshift  30179  spansncvi  31588  eigposi  31772  pjnormssi  32104  sumdmdlem  32354  tngdim  33616  bnj168  34727  bnj964  34940  bnj966  34941  bnj1398  35031  fnrelpredd  35086  lfuhgr3  35114  acycgrislfgr  35146  cgrdegen  35999  btwnconn1lem11  36092  btwnconn1lem12  36093  btwnconn1lem14  36095  bj-opelidb1  37148  bj-inexeqex  37149  bj-idreseqb  37158  bj-ideqg1ALT  37160  bj-ccinftydisj  37208  phpreu  37605  fin2so  37608  matunitlindflem2  37618  poimirlem26  37647  poimirlem28  37649  dvasin  37705  isbnd2  37784  atcvrj0  39429  paddasslem5  39825  expeq1d  42319  pm13.13a  44403  iotavalb  44426  suctrALTcf  44918  suctrALTcfVD  44919  suctrALT3  44920  unisnALT  44922  2sb5ndALT  44928  xreqle  45322  supminfxr2  45472  fourierdlem40  46152  fourierdlem78  46189  tz6.12-afv2  47245  afv2fv0  47270  2ffzoeq  47332  clnbgrval  47827  dfsclnbgr6  47862  uspgrlimlem1  47991  uspgropssxp  48136  uspgrsprfo  48140  nn0sumshdiglemA  48612  itscnhlc0yqe  48752