Theorem biimpac 484

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  r19.29r  3131  gencbvex2  3514  2reu5  3723  sseq0  4361  ifpprsnss  4732  dfiun2g  4996  poltletr  6134  ordnbtwn  6460  funopsn  7150  funopsnOLD  7151  onsucuni2  7836  1stconst  8101  2ndconst  8102  smo11  8357  omlimcl  8569  omxpenlem  9073  fodomr  9123  f1oenfirn  9171  f1domfi  9172  fodomfib  9295  infsupprpr  9473  r1val1  9765  alephval3  10110  dfac5lem4  10126  dfac5  10128  axdc4lem  10454  fodomb  10525  distrlem1pr  11027  map2psrpr  11112  supsrlem  11113  eqle  11329  swrd0  14720  repswswrd  14847  cshwidxmod  14866  rtrclind  15128  sumz  15798  prod1  16023  divalglem8  16482  flodddiv4  16497  pospo  18423  mgm2nsgrplem2  19020  eqg0subg  19313  rhmdvdsr  20657  lsmcv  21317  sraring  21359  opsrtoslem1  22258  madugsum  22852  hauscmplem  23615  bwth  23619  ptbasfi  23791  hmphindis  24007  fbncp  24049  fgcl  24088  fixufil  24132  uffixfr  24133  mbfima  25842  mbfimaicc  25843  ig1pdvds  26390  zabsle1  27513  tgldimor  28824  ax5seglem4  29339  axcontlem2  29372  axcontlem4  29374  lfuhgr3  29557  nbgrval  29746  cusgrfi  29868  fusgrregdegfi  29979  rusgr1vtxlem  29997  wlkiswwlksupgr2  30295  elwwlks2ons3  30373  clwwlknonwwlknonb  30526  eucrctshift  30667  spansncvi  32077  eigposi  32261  pjnormssi  32593  sumdmdlem  32843  tngdim  34069  bnj168  35186  bnj964  35398  bnj966  35399  bnj1398  35489  fnrelpredd  35542  acycgrislfgr  35683  cgrdegen  36535  btwnconn1lem11  36628  btwnconn1lem12  36629  btwnconn1lem14  36631  bj-opelidb1  37856  bj-inexeqex  37857  bj-idreseqb  37866  bj-ideqg1ALT  37868  bj-ccinftydisj  37916  phpreu  38314  fin2so  38317  matunitlindflem2  38327  poimirlem26  38356  poimirlem28  38358  dvasin  38414  isbnd2  38494  atcvrj0  40262  paddasslem5  40658  expeq1d  43145  pm13.13a  45177  iotavalb  45200  suctrALTcf  45690  suctrALTcfVD  45691  suctrALT3  45692  unisnALT  45694  2sb5ndALT  45700  xreqle  46096  supminfxr2  46243  fourierdlem40  46921  fourierdlem78  46958  tz6.12-afv2  48037  afv2fv0  48062  2ffzoeq  48125  clnbgrval  48647  dfsclnbgr6  48683  uspgrlimlem1  48813  uspgropssxp  48969  uspgrsprfo  48973  nn0sumshdiglemA  49458  itscnhlc0yqe  49598