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  3715  sseq0  4353  ifpprsnss  4721  dfiun2g  4987  poltletr  6128  ordnbtwn  6461  funopsn  7156  funopsnOLD  7157  onsucuni2  7849  1stconst  8118  2ndconst  8119  smo11  8380  omlimcl  8594  omxpenlem  9105  fodomr  9155  f1oenfirn  9203  f1domfi  9204  fodomfib  9328  infsupprpr  9505  r1val1  9800  alephval3  10196  dfac5lem4  10212  dfac5  10214  axdc4lem  10540  fodomb  10612  distrlem1pr  11117  map2psrpr  11202  supsrlem  11203  eqle  11419  swrd0  14816  repswswrd  14943  cshwidxmod  14962  rtrclind  15227  sumz  15897  prod1  16120  divalglem8  16579  flodddiv4  16594  pospo  18526  mgm2nsgrplem2  19127  eqg0subg  19420  rhmdvdsr  20767  lsmcv  21428  sraring  21470  opsrtoslem1  22373  madugsum  22967  matunitlindflem2  23004  hauscmplem  23733  bwth  23737  ptbasfi  23909  hmphindis  24125  fbncp  24167  fgcl  24206  fixufil  24250  uffixfr  24251  mbfima  25960  mbfimaicc  25961  ig1pdvds  26507  zabsle1  27632  tgldimor  28974  ax5seglem4  29519  axcontlem2  29552  axcontlem4  29554  lfuhgr3  29737  nbgrval  29926  cusgrfi  30048  fusgrregdegfi  30159  rusgr1vtxlem  30177  wlkiswwlksupgr2  30475  elwwlks2ons3  30553  clwwlknonwwlknonb  30706  eucrctshift  30853  spansncvi  32263  eigposi  32447  pjnormssi  32779  sumdmdlem  33029  tngdim  34295  bnj168  35411  bnj964  35623  bnj966  35624  bnj1398  35714  fnrelpredd  35778  acwer1prc  35828  acycgrislfgr  36025  cgrdegen  36893  btwnconn1lem11  36986  btwnconn1lem12  36987  btwnconn1lem14  36989  bj-opelidb1  38211  bj-inexeqex  38212  bj-idreseqb  38221  bj-ideqg1ALT  38223  bj-ccinftydisj  38271  phpreu  38664  fin2so  38667  poimirlem26  38701  poimirlem28  38703  dvasin  38759  isbnd2  38854  atcvrj0  40622  paddasslem5  41018  expeq1d  43518  pm13.13a  45528  iotavalb  45550  suctrALTcf  46040  suctrALTcfVD  46041  suctrALT3  46042  unisnALT  46044  2sb5ndALT  46050  xreqle  46468  supminfxr2  46615  fourierdlem40  47293  fourierdlem78  47330  tz6.12-afv2  48446  afv2fv0  48471  2ffzoeq  48534  clnbgrval  49056  dfsclnbgr6  49092  uspgrlimlem1  49222  uspgropssxp  49378  uspgrsprfo  49382  nn0sumshdiglemA  49867  itscnhlc0yqe  50007