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  3096  gencbvex2  3496  2reu5  3712  ifpprsnss  4714  dfiun2g  4978  poltletr  6078  ordnbtwn  6401  funopsn  7081  onsucuni2  7764  1stconst  8030  2ndconst  8031  smo11  8284  omlimcl  8493  omxpenlem  8991  fodomr  9041  f1oenfirn  9089  f1domfi  9090  fodomfib  9213  fodomfibOLD  9215  infsupprpr  9390  r1val1  9679  alephval3  10001  dfac5lem4  10017  dfac5lem4OLD  10019  dfac5  10020  axdc4lem  10346  fodomb  10417  distrlem1pr  10916  map2psrpr  11001  supsrlem  11002  eqle  11215  swrd0  14566  repswswrd  14691  cshwidxmod  14710  rtrclind  14972  sumz  15629  prod1  15851  divalglem8  16311  flodddiv4  16326  pospo  18249  mgm2nsgrplem2  18827  eqg0subg  19108  rhmdvdsr  20423  lsmcv  21078  sraring  21120  opsrtoslem1  21990  madugsum  22558  hauscmplem  23321  bwth  23325  ptbasfi  23496  hmphindis  23712  fbncp  23754  fgcl  23793  fixufil  23837  uffixfr  23838  mbfima  25558  mbfimaicc  25559  ig1pdvds  26112  zabsle1  27234  tgldimor  28480  ax5seglem4  28910  axcontlem2  28943  axcontlem4  28945  nbgrval  29314  cusgrfi  29437  fusgrregdegfi  29548  rusgr1vtxlem  29566  wlkiswwlksupgr2  29855  elwwlks2ons3  29933  clwwlknonwwlknonb  30086  eucrctshift  30223  spansncvi  31632  eigposi  31816  pjnormssi  32148  sumdmdlem  32398  tngdim  33626  bnj168  34742  bnj964  34955  bnj966  34956  bnj1398  35046  fnrelpredd  35102  lfuhgr3  35164  acycgrislfgr  35196  cgrdegen  36048  btwnconn1lem11  36141  btwnconn1lem12  36142  btwnconn1lem14  36144  bj-opelidb1  37197  bj-inexeqex  37198  bj-idreseqb  37207  bj-ideqg1ALT  37209  bj-ccinftydisj  37257  phpreu  37654  fin2so  37657  matunitlindflem2  37667  poimirlem26  37696  poimirlem28  37698  dvasin  37754  isbnd2  37833  atcvrj0  39537  paddasslem5  39933  expeq1d  42427  pm13.13a  44510  iotavalb  44533  suctrALTcf  45024  suctrALTcfVD  45025  suctrALT3  45026  unisnALT  45028  2sb5ndALT  45034  xreqle  45428  supminfxr2  45577  fourierdlem40  46255  fourierdlem78  46292  tz6.12-afv2  47350  afv2fv0  47375  2ffzoeq  47437  clnbgrval  47932  dfsclnbgr6  47968  uspgrlimlem1  48098  uspgropssxp  48254  uspgrsprfo  48258  nn0sumshdiglemA  48730  itscnhlc0yqe  48870