Theorem biimpac 483

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 411	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  r19.29r  3129  gencbvex2  3512  2reu5  3721  sseq0  4361  ifpprsnss  4730  dfiun2g  4994  poltletr  6132  ordnbtwn  6456  funopsn  7144  funopsnOLD  7145  onsucuni2  7826  1stconst  8091  2ndconst  8092  smo11  8347  omlimcl  8559  omxpenlem  9062  fodomr  9112  f1oenfirn  9160  f1domfi  9161  fodomfib  9284  infsupprpr  9462  r1val1  9754  alephval3  10090  dfac5lem4  10106  dfac5  10108  axdc4lem  10434  fodomb  10505  distrlem1pr  11005  map2psrpr  11090  supsrlem  11091  eqle  11307  swrd0  14692  repswswrd  14817  cshwidxmod  14836  rtrclind  15098  sumz  15769  prod1  15994  divalglem8  16453  flodddiv4  16468  pospo  18394  mgm2nsgrplem2  18976  eqg0subg  19262  rhmdvdsr  20605  lsmcv  21265  sraring  21307  opsrtoslem1  22206  madugsum  22800  hauscmplem  23563  bwth  23567  ptbasfi  23738  hmphindis  23954  fbncp  23996  fgcl  24035  fixufil  24079  uffixfr  24080  mbfima  25789  mbfimaicc  25790  ig1pdvds  26337  zabsle1  27460  tgldimor  28771  ax5seglem4  29282  axcontlem2  29315  axcontlem4  29317  nbgrval  29686  cusgrfi  29808  fusgrregdegfi  29919  rusgr1vtxlem  29937  wlkiswwlksupgr2  30226  elwwlks2ons3  30304  clwwlknonwwlknonb  30457  eucrctshift  30594  spansncvi  32004  eigposi  32188  pjnormssi  32520  sumdmdlem  32770  tngdim  34003  bnj168  35119  bnj964  35331  bnj966  35332  bnj1398  35422  fnrelpredd  35482  lfuhgr3  35612  acycgrislfgr  35644  cgrdegen  36496  btwnconn1lem11  36589  btwnconn1lem12  36590  btwnconn1lem14  36592  bj-opelidb1  37817  bj-inexeqex  37818  bj-idreseqb  37827  bj-ideqg1ALT  37829  bj-ccinftydisj  37877  phpreu  38275  fin2so  38278  matunitlindflem2  38288  poimirlem26  38317  poimirlem28  38319  dvasin  38375  isbnd2  38454  atcvrj0  40222  paddasslem5  40618  expeq1d  43105  pm13.13a  45137  iotavalb  45160  suctrALTcf  45650  suctrALTcfVD  45651  suctrALT3  45652  unisnALT  45654  2sb5ndALT  45660  xreqle  46056  supminfxr2  46203  fourierdlem40  46881  fourierdlem78  46918  tz6.12-afv2  47997  afv2fv0  48022  2ffzoeq  48085  clnbgrval  48607  dfsclnbgr6  48643  uspgrlimlem1  48773  uspgropssxp  48929  uspgrsprfo  48933  nn0sumshdiglemA  49419  itscnhlc0yqe  49559