Theorem biimpac 481

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 251	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 409	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  gencbvex2  3550  2reu5  3748  ifpprsnss  4693  poltletr  5986  ordnbtwn  6275  tz6.12-1  6686  funopsn  6904  onsucuni2  7543  1stconst  7789  2ndconst  7790  smo11  7995  omlimcl  8198  omxpenlem  8612  fodomr  8662  fodomfib  8792  infsupprpr  8962  r1val1  9209  alephval3  9530  dfac5lem4  9546  dfac5  9548  axdc4lem  9871  fodomb  9942  distrlem1pr  10441  map2psrpr  10526  supsrlem  10527  eqle  10736  swrd0  14014  repswswrd  14140  cshwidxmod  14159  rtrclind  14418  sumz  15073  prod1  15292  divalglem8  15745  flodddiv4  15758  pospo  17577  mgm2nsgrplem2  18078  lsmcv  19907  opsrtoslem1  20258  psrbagfsupp  20283  madugsum  21246  hauscmplem  22008  bwth  22012  ptbasfi  22183  hmphindis  22399  fbncp  22441  fgcl  22480  fixufil  22524  uffixfr  22525  mbfima  24225  mbfimaicc  24226  ig1pdvds  24764  zabsle1  25866  tgldimor  26282  ax5seglem4  26712  axcontlem2  26745  axcontlem4  26747  nbgrval  27112  cusgrfi  27234  fusgrregdegfi  27345  rusgr1vtxlem  27363  wlkiswwlksupgr2  27649  elwwlks2ons3  27728  clwwlknonwwlknonb  27879  eucrctshift  28016  spansncvi  29423  eigposi  29607  pjnormssi  29939  sumdmdlem  30189  rhmdvdsr  30886  sraring  30982  tngdim  31006  bnj168  31995  bnj521  32002  bnj964  32210  bnj966  32211  bnj1398  32301  lfuhgr3  32361  acycgrislfgr  32394  cgrdegen  33460  btwnconn1lem11  33553  btwnconn1lem12  33554  btwnconn1lem14  33556  bj-opelidb1  34439  bj-inexeqex  34440  bj-idreseqb  34449  bj-ideqg1ALT  34451  bj-ccinftydisj  34489  phpreu  34870  fin2so  34873  matunitlindflem2  34883  poimirlem26  34912  poimirlem28  34914  dvasin  34972  isbnd2  35055  atcvrj0  36558  paddasslem5  36954  pm13.13a  40732  iotavalb  40755  suctrALTcf  41249  suctrALTcfVD  41250  suctrALT3  41251  unisnALT  41253  2sb5ndALT  41259  xreqle  41579  supminfxr2  41738  fourierdlem40  42426  fourierdlem78  42463  tz6.12-afv2  43433  afv2fv0  43458  2ffzoeq  43522  uspgropssxp  44013  uspgrsprfo  44017  difmodm1lt  44576  nn0sumshdiglemA  44673  itscnhlc0yqe  44740