Theorem mpd3an3 1465

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 1119	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpdan 688	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  stoic2b  1777  elovmpo  7612  f1oeng  8917  php  9141  nnsdomg  9209  wdomimag  9502  gruuni  10723  genpv  10922  pncan3  11401  mulsubaddmulsub  11614  infssuzle  12881  fzrevral3  13568  flflp1  13766  subsq2  14173  brfi1ind  14471  opfi1ind  14474  ccatws1ls  14596  swrdrlen  14622  pfxpfxid  14671  pfxcctswrd  14672  2cshwid  14776  caubnd  15321  dvdsmul1  16246  dvdsmul2  16247  hashbcval  16973  setsvalg  17136  ressval  17203  restval  17389  mrelatglb0  18527  imasmnd2  18742  efmndov  18849  qusinv  19165  ghminv  19198  gsmsymgrfixlem1  19402  gsmsymgreqlem2  19406  gexod  19561  lsmvalx  19614  rngrz  20147  imasring  20310  irredneg  20410  01eq0ring  20507  ocvin  21654  frlmiscvec  21829  evlrhm  22079  gsumsmonply1  22272  mat1mhm  22449  marrepfval  22525  marrepval0  22526  marepvfval  22530  marepvval0  22531  1elcpmat  22680  m2cpminv0  22726  idpm2idmp  22766  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  restin  23131  qtopval  23660  elqtop3  23668  elfm3  23915  flimval  23928  nmge0  24582  nmeq0  24583  nminv  24586  nmo0  24700  0nghm  24706  coemulhi  26219  isosctrlem2  26783  divsqrtsumlem  26943  2lgsoddprmlem4  27378  0uhgrrusgr  29647  frgruhgr0v  30334  nvge0  30744  nvnd  30759  dip0r  30788  dip0l  30789  nmoo0  30862  hi2eq  31176  wrdsplex  32996  resvval  33389  unitdivcld  34045  signspval  34696  satfv0  35540  ltflcei  37929  elghomlem1OLD  38206  rngorz  38244  rngonegmn1l  38262  rngonegmn1r  38263  igenval  38382  xrnidresex  38751  xrncnvepresex  38752  lfl0  39511  olj01  39671  olm11  39673  hl2at  39851  pmapeq0  40212  trlcl  40610  trlle  40630  tendoid  41219  tendo0plr  41238  tendoipl2  41244  erngmul  41252  erngmul-rN  41260  dvamulr  41458  dvavadd  41461  dvhmulr  41532  cdlemm10N  41564  repncan3  42815  pellfund14  43326  mendmulr  43612  onnoxpg  43856  fmuldfeq  46013  stoweidlem19  46447  stoweidlem26  46454  addsubeq0  47744  zp1modne  47800  modm1nep1  47819  prelspr  47946  lincval1  48895