Theorem biimpac 478

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  r19.29r  3093  gencbvex2  3497  2reu5  3718  ifpprsnss  4716  dfiun2g  4980  poltletr  6081  ordnbtwn  6402  funopsn  7082  onsucuni2  7767  1stconst  8033  2ndconst  8034  smo11  8287  omlimcl  8496  omxpenlem  8995  fodomr  9045  f1oenfirn  9094  f1domfi  9095  fodomfib  9219  fodomfibOLD  9221  infsupprpr  9396  r1val1  9682  alephval3  10004  dfac5lem4  10020  dfac5lem4OLD  10022  dfac5  10023  axdc4lem  10349  fodomb  10420  distrlem1pr  10919  map2psrpr  11004  supsrlem  11005  eqle  11218  swrd0  14565  repswswrd  14690  cshwidxmod  14709  rtrclind  14972  sumz  15629  prod1  15851  divalglem8  16311  flodddiv4  16326  pospo  18249  mgm2nsgrplem2  18793  eqg0subg  19075  rhmdvdsr  20393  lsmcv  21048  sraring  21090  opsrtoslem1  21960  madugsum  22528  hauscmplem  23291  bwth  23295  ptbasfi  23466  hmphindis  23682  fbncp  23724  fgcl  23763  fixufil  23807  uffixfr  23808  mbfima  25529  mbfimaicc  25530  ig1pdvds  26083  zabsle1  27205  tgldimor  28447  ax5seglem4  28877  axcontlem2  28910  axcontlem4  28912  nbgrval  29281  cusgrfi  29404  fusgrregdegfi  29515  rusgr1vtxlem  29533  wlkiswwlksupgr2  29822  elwwlks2ons3  29900  clwwlknonwwlknonb  30050  eucrctshift  30187  spansncvi  31596  eigposi  31780  pjnormssi  32112  sumdmdlem  32362  tngdim  33580  bnj168  34697  bnj964  34910  bnj966  34911  bnj1398  35001  fnrelpredd  35056  lfuhgr3  35097  acycgrislfgr  35129  cgrdegen  35982  btwnconn1lem11  36075  btwnconn1lem12  36076  btwnconn1lem14  36078  bj-opelidb1  37131  bj-inexeqex  37132  bj-idreseqb  37141  bj-ideqg1ALT  37143  bj-ccinftydisj  37191  phpreu  37588  fin2so  37591  matunitlindflem2  37601  poimirlem26  37630  poimirlem28  37632  dvasin  37688  isbnd2  37767  atcvrj0  39411  paddasslem5  39807  expeq1d  42301  pm13.13a  44384  iotavalb  44407  suctrALTcf  44899  suctrALTcfVD  44900  suctrALT3  44901  unisnALT  44903  2sb5ndALT  44909  xreqle  45303  supminfxr2  45452  fourierdlem40  46132  fourierdlem78  46169  tz6.12-afv2  47228  afv2fv0  47253  2ffzoeq  47315  clnbgrval  47810  dfsclnbgr6  47846  uspgrlimlem1  47976  uspgropssxp  48132  uspgrsprfo  48136  nn0sumshdiglemA  48608  itscnhlc0yqe  48748