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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  gencbvex2  3479  2reu5  3688  ifpprsnss  4697  poltletr  6026  ordnbtwn  6341  tz6.12-1  6778  funopsn  7002  onsucuni2  7656  1stconst  7911  2ndconst  7912  smo11  8166  omlimcl  8371  omxpenlem  8813  fodomr  8864  f1oenfirn  8927  f1domfi  8928  fodomfib  9023  infsupprpr  9193  r1val1  9475  alephval3  9797  dfac5lem4  9813  dfac5  9815  axdc4lem  10142  fodomb  10213  distrlem1pr  10712  map2psrpr  10797  supsrlem  10798  eqle  11007  swrd0  14299  repswswrd  14425  cshwidxmod  14444  rtrclind  14704  sumz  15362  prod1  15582  divalglem8  16037  flodddiv4  16050  pospo  17978  mgm2nsgrplem2  18473  lsmcv  20318  psrbagfsuppOLD  21034  opsrtoslem1  21172  madugsum  21700  hauscmplem  22465  bwth  22469  ptbasfi  22640  hmphindis  22856  fbncp  22898  fgcl  22937  fixufil  22981  uffixfr  22982  mbfima  24699  mbfimaicc  24700  ig1pdvds  25246  zabsle1  26349  tgldimor  26767  ax5seglem4  27203  axcontlem2  27236  axcontlem4  27238  nbgrval  27606  cusgrfi  27728  fusgrregdegfi  27839  rusgr1vtxlem  27857  wlkiswwlksupgr2  28143  elwwlks2ons3  28221  clwwlknonwwlknonb  28371  eucrctshift  28508  spansncvi  29915  eigposi  30099  pjnormssi  30431  sumdmdlem  30681  rhmdvdsr  31419  sraring  31574  tngdim  31598  bnj168  32609  bnj521  32616  bnj964  32823  bnj966  32824  bnj1398  32914  fnrelpredd  32961  lfuhgr3  32981  acycgrislfgr  33014  cgrdegen  34233  btwnconn1lem11  34326  btwnconn1lem12  34327  btwnconn1lem14  34329  bj-opelidb1  35251  bj-inexeqex  35252  bj-idreseqb  35261  bj-ideqg1ALT  35263  bj-ccinftydisj  35311  phpreu  35688  fin2so  35691  matunitlindflem2  35701  poimirlem26  35730  poimirlem28  35732  dvasin  35788  isbnd2  35868  atcvrj0  37369  paddasslem5  37765  pm13.13a  41914  iotavalb  41937  suctrALTcf  42431  suctrALTcfVD  42432  suctrALT3  42433  unisnALT  42435  2sb5ndALT  42441  xreqle  42747  supminfxr2  42899  fourierdlem40  43578  fourierdlem78  43615  tz6.12-afv2  44619  afv2fv0  44644  2ffzoeq  44708  uspgropssxp  45194  uspgrsprfo  45198  difmodm1lt  45756  nn0sumshdiglemA  45853  itscnhlc0yqe  45993