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  3126  gencbvex2  3507  2reu5  3716  sseq0  4354  ifpprsnss  4725  dfiun2g  4988  poltletr  6126  ordnbtwn  6453  funopsn  7145  funopsnOLD  7146  onsucuni2  7831  1stconst  8098  2ndconst  8099  smo11  8354  omlimcl  8566  omxpenlem  9077  fodomr  9127  f1oenfirn  9175  f1domfi  9176  fodomfib  9299  infsupprpr  9477  r1val1  9769  alephval3  10114  dfac5lem4  10130  dfac5  10132  axdc4lem  10458  fodomb  10530  distrlem1pr  11035  map2psrpr  11120  supsrlem  11121  eqle  11337  swrd0  14729  repswswrd  14856  cshwidxmod  14875  rtrclind  15139  sumz  15809  prod1  16032  divalglem8  16491  flodddiv4  16506  pospo  18432  mgm2nsgrplem2  19032  eqg0subg  19325  rhmdvdsr  20669  lsmcv  21329  sraring  21371  opsrtoslem1  22272  madugsum  22866  matunitlindflem2  22903  hauscmplem  23632  bwth  23636  ptbasfi  23808  hmphindis  24024  fbncp  24066  fgcl  24105  fixufil  24149  uffixfr  24150  mbfima  25859  mbfimaicc  25860  ig1pdvds  26406  zabsle1  27533  tgldimor  28845  ax5seglem4  29390  axcontlem2  29423  axcontlem4  29425  lfuhgr3  29608  nbgrval  29797  cusgrfi  29919  fusgrregdegfi  30030  rusgr1vtxlem  30048  wlkiswwlksupgr2  30346  elwwlks2ons3  30424  clwwlknonwwlknonb  30577  eucrctshift  30724  spansncvi  32134  eigposi  32318  pjnormssi  32650  sumdmdlem  32900  tngdim  34124  bnj168  35241  bnj964  35453  bnj966  35454  bnj1398  35544  fnrelpredd  35597  acycgrislfgr  35732  cgrdegen  36585  btwnconn1lem11  36678  btwnconn1lem12  36679  btwnconn1lem14  36681  bj-opelidb1  37906  bj-inexeqex  37907  bj-idreseqb  37916  bj-ideqg1ALT  37918  bj-ccinftydisj  37966  phpreu  38359  fin2so  38362  poimirlem26  38396  poimirlem28  38398  dvasin  38454  isbnd2  38534  atcvrj0  40302  paddasslem5  40698  expeq1d  43200  pm13.13a  45232  iotavalb  45255  suctrALTcf  45745  suctrALTcfVD  45746  suctrALT3  45747  unisnALT  45749  2sb5ndALT  45755  xreqle  46151  supminfxr2  46298  fourierdlem40  46976  fourierdlem78  47013  tz6.12-afv2  48129  afv2fv0  48154  2ffzoeq  48217  clnbgrval  48739  dfsclnbgr6  48775  uspgrlimlem1  48905  uspgropssxp  49061  uspgrsprfo  49065  nn0sumshdiglemA  49550  itscnhlc0yqe  49690