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  3135  gencbvex2  3520  2reu5  3730  ifpprsnss  4735  dfiun2g  4998  poltletr  6133  ordnbtwn  6457  funopsn  7145  funopsnOLD  7146  onsucuni2  7830  1stconst  8095  2ndconst  8096  smo11  8351  omlimcl  8563  omxpenlem  9066  fodomr  9116  f1oenfirn  9164  f1domfi  9165  fodomfib  9288  infsupprpr  9466  r1val1  9758  alephval3  10094  dfac5lem4  10110  dfac5  10112  axdc4lem  10439  fodomb  10510  distrlem1pr  11010  map2psrpr  11095  supsrlem  11096  eqle  11312  swrd0  14696  repswswrd  14821  cshwidxmod  14840  rtrclind  15102  sumz  15773  prod1  15998  divalglem8  16458  flodddiv4  16473  pospo  18399  mgm2nsgrplem2  18981  eqg0subg  19267  rhmdvdsr  20591  lsmcv  21243  sraring  21285  opsrtoslem1  22175  madugsum  22769  hauscmplem  23532  bwth  23536  ptbasfi  23707  hmphindis  23923  fbncp  23965  fgcl  24004  fixufil  24048  uffixfr  24049  mbfima  25758  mbfimaicc  25759  ig1pdvds  26306  zabsle1  27426  tgldimor  28737  ax5seglem4  29223  axcontlem2  29256  axcontlem4  29258  nbgrval  29627  cusgrfi  29749  fusgrregdegfi  29860  rusgr1vtxlem  29878  wlkiswwlksupgr2  30167  elwwlks2ons3  30245  clwwlknonwwlknonb  30398  eucrctshift  30535  spansncvi  31945  eigposi  32129  pjnormssi  32461  sumdmdlem  32711  tngdim  33948  bnj168  35064  bnj964  35276  bnj966  35277  bnj1398  35367  fnrelpredd  35425  lfuhgr3  35511  acycgrislfgr  35543  cgrdegen  36395  btwnconn1lem11  36488  btwnconn1lem12  36489  btwnconn1lem14  36491  bj-opelidb1  37685  bj-inexeqex  37686  bj-idreseqb  37695  bj-ideqg1ALT  37697  bj-ccinftydisj  37745  phpreu  38143  fin2so  38146  matunitlindflem2  38156  poimirlem26  38185  poimirlem28  38187  dvasin  38243  isbnd2  38322  atcvrj0  40092  paddasslem5  40488  expeq1d  42975  pm13.13a  45009  iotavalb  45032  suctrALTcf  45522  suctrALTcfVD  45523  suctrALT3  45524  unisnALT  45526  2sb5ndALT  45532  xreqle  45928  supminfxr2  46075  fourierdlem40  46753  fourierdlem78  46790  tz6.12-afv2  47866  afv2fv0  47891  2ffzoeq  47954  clnbgrval  48476  dfsclnbgr6  48512  uspgrlimlem1  48642  uspgropssxp  48798  uspgrsprfo  48802  nn0sumshdiglemA  49284  itscnhlc0yqe  49424