Theorem mpd3an3 1459

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  stoic2b  1777  elovmpo  7370  f1oeng  8511  wdomimag  9035  gruuni  10211  genpv  10410  pncan3  10883  mulsubaddmulsub  11093  infssuzle  12319  fzrevral3  12989  flflp1  13172  subsq2  13569  brfi1ind  13853  opfi1ind  13856  ccatws1ls  13983  swrdrlen  14012  pfxpfxid  14062  pfxcctswrd  14063  2cshwid  14167  caubnd  14710  dvdsmul1  15623  dvdsmul2  15624  hashbcval  16328  setsvalg  16504  ressval  16543  restval  16692  mrelatglb0  17787  imasmnd2  17940  efmndov  18038  qusinv  18331  ghminv  18357  gsmsymgrfixlem1  18547  gsmsymgreqlem2  18551  gexod  18703  lsmvalx  18756  ringrz  19334  imasring  19365  irredneg  19456  ocvin  20363  frlmiscvec  20538  evlrhm  20768  gsumsmonply1  20932  mat1mhm  21089  marrepfval  21165  marrepval0  21166  marepvfval  21170  marepvval0  21171  1elcpmat  21320  m2cpminv0  21366  idpm2idmp  21406  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  restin  21771  qtopval  22300  elqtop3  22308  elfm3  22555  flimval  22568  nmge0  23223  nmeq0  23224  nminv  23227  nmo0  23341  0nghm  23347  coemulhi  24851  isosctrlem2  25405  divsqrtsumlem  25565  2lgsoddprmlem4  25999  0uhgrrusgr  27368  frgruhgr0v  28049  nvge0  28456  nvnd  28471  dip0r  28500  dip0l  28501  nmoo0  28574  hi2eq  28888  wrdsplex  30640  resvval  30951  unitdivcld  31254  signspval  31932  satfv0  32718  ltflcei  35045  elghomlem1OLD  35323  rngorz  35361  rngonegmn1l  35379  rngonegmn1r  35380  igenval  35499  xrnidresex  35815  xrncnvepresex  35816  lfl0  36361  olj01  36521  olm11  36523  hl2at  36701  pmapeq0  37062  trlcl  37460  trlle  37480  tendoid  38069  tendo0plr  38088  tendoipl2  38094  erngmul  38102  erngmul-rN  38110  dvamulr  38308  dvavadd  38311  dvhmulr  38382  cdlemm10N  38414  repncan3  39521  pellfund14  39839  mendmulr  40132  fmuldfeq  42225  stoweidlem19  42661  stoweidlem26  42668  addsubeq0  43853  prelspr  44003  lincval1  44828