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  3127  gencbvex2  3508  2reu5  3716  sseq0  4354  ifpprsnss  4725  dfiun2g  4988  poltletr  6126  ordnbtwn  6458  funopsn  7151  funopsnOLD  7152  onsucuni2  7845  1stconst  8111  2ndconst  8112  smo11  8372  omlimcl  8586  omxpenlem  9097  fodomr  9147  f1oenfirn  9195  f1domfi  9196  fodomfib  9320  infsupprpr  9498  r1val1  9793  alephval3  10189  dfac5lem4  10205  dfac5  10207  axdc4lem  10533  fodomb  10605  distrlem1pr  11110  map2psrpr  11195  supsrlem  11196  eqle  11412  swrd0  14808  repswswrd  14935  cshwidxmod  14954  rtrclind  15218  sumz  15888  prod1  16111  divalglem8  16570  flodddiv4  16585  pospo  18517  mgm2nsgrplem2  19118  eqg0subg  19411  rhmdvdsr  20758  lsmcv  21419  sraring  21461  opsrtoslem1  22364  madugsum  22958  matunitlindflem2  22995  hauscmplem  23724  bwth  23728  ptbasfi  23900  hmphindis  24116  fbncp  24158  fgcl  24197  fixufil  24241  uffixfr  24242  mbfima  25951  mbfimaicc  25952  ig1pdvds  26498  zabsle1  27623  tgldimor  28965  ax5seglem4  29510  axcontlem2  29543  axcontlem4  29545  lfuhgr3  29728  nbgrval  29917  cusgrfi  30039  fusgrregdegfi  30150  rusgr1vtxlem  30168  wlkiswwlksupgr2  30466  elwwlks2ons3  30544  clwwlknonwwlknonb  30697  eucrctshift  30844  spansncvi  32254  eigposi  32438  pjnormssi  32770  sumdmdlem  33020  tngdim  34245  bnj168  35361  bnj964  35573  bnj966  35574  bnj1398  35664  fnrelpredd  35720  acwer1prc  35760  acycgrislfgr  35917  cgrdegen  36769  btwnconn1lem11  36862  btwnconn1lem12  36863  btwnconn1lem14  36865  bj-opelidb1  38074  bj-inexeqex  38075  bj-idreseqb  38084  bj-ideqg1ALT  38086  bj-ccinftydisj  38134  phpreu  38527  fin2so  38530  poimirlem26  38564  poimirlem28  38566  dvasin  38622  isbnd2  38717  atcvrj0  40485  paddasslem5  40881  expeq1d  43381  pm13.13a  45390  iotavalb  45413  suctrALTcf  45903  suctrALTcfVD  45904  suctrALT3  45905  unisnALT  45907  2sb5ndALT  45913  xreqle  46331  supminfxr2  46478  fourierdlem40  47156  fourierdlem78  47193  tz6.12-afv2  48309  afv2fv0  48334  2ffzoeq  48397  clnbgrval  48919  dfsclnbgr6  48955  uspgrlimlem1  49085  uspgropssxp  49241  uspgrsprfo  49245  nn0sumshdiglemA  49730  itscnhlc0yqe  49870