Theorem mpd3an3 1462

Description: An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)

Hypotheses

Ref	Expression
mpd3an3.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
mpd3an3.3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mpd3an3	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem mpd3an3

Step	Hyp	Ref	Expression
1		mpd3an3.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2		mpd3an3.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expa 1118	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpdan 685	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  stoic2b  1777  elovmpo  7653  f1oeng  8969  php  9212  nnsdomg  9304  wdomimag  9584  gruuni  10797  genpv  10996  pncan3  11472  mulsubaddmulsub  11682  infssuzle  12919  fzrevral3  13592  flflp1  13776  subsq2  14179  brfi1ind  14464  opfi1ind  14467  ccatws1ls  14587  swrdrlen  14613  pfxpfxid  14663  pfxcctswrd  14664  2cshwid  14768  caubnd  15309  dvdsmul1  16225  dvdsmul2  16226  hashbcval  16939  setsvalg  17103  ressval  17180  restval  17376  mrelatglb0  18518  imasmnd2  18696  efmndov  18798  qusinv  19105  ghminv  19137  gsmsymgrfixlem1  19336  gsmsymgreqlem2  19340  gexod  19495  lsmvalx  19548  rngrz  20060  imasring  20218  irredneg  20321  01eq0ring  20419  ocvin  21446  frlmiscvec  21623  evlrhm  21878  gsumsmonply1  22047  mat1mhm  22206  marrepfval  22282  marrepval0  22283  marepvfval  22287  marepvval0  22288  1elcpmat  22437  m2cpminv0  22483  idpm2idmp  22523  chfacfscmulgsum  22582  chfacfpmmulgsum  22586  restin  22890  qtopval  23419  elqtop3  23427  elfm3  23674  flimval  23687  nmge0  24346  nmeq0  24347  nminv  24350  nmo0  24472  0nghm  24478  coemulhi  25992  isosctrlem2  26548  divsqrtsumlem  26708  2lgsoddprmlem4  27142  0uhgrrusgr  29090  frgruhgr0v  29772  nvge0  30181  nvnd  30196  dip0r  30225  dip0l  30226  nmoo0  30299  hi2eq  30613  wrdsplex  32359  resvval  32699  unitdivcld  33167  signspval  33849  satfv0  34635  ltflcei  36779  elghomlem1OLD  37056  rngorz  37094  rngonegmn1l  37112  rngonegmn1r  37113  igenval  37232  xrnidresex  37580  xrncnvepresex  37581  lfl0  38238  olj01  38398  olm11  38400  hl2at  38579  pmapeq0  38940  trlcl  39338  trlle  39358  tendoid  39947  tendo0plr  39966  tendoipl2  39972  erngmul  39980  erngmul-rN  39988  dvamulr  40186  dvavadd  40189  dvhmulr  40260  cdlemm10N  40292  repncan3  41558  pellfund14  41938  mendmulr  42232  onnog  42482  fmuldfeq  44598  stoweidlem19  45034  stoweidlem26  45041  addsubeq0  46303  prelspr  46453  lincval1  47188