Theorem mpd3an3 1491

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  stoic2b  1807  elovmpo  7666  f1oeng  8997  php  9222  nnsdomg  9291  wdomimag  9581  gruuni  10885  genpv  11084  pncan3  11565  mulsubaddmulsub  11780  infssuzle  13058  fzrevral3  13748  flflp1  13947  subsq2  14355  brfi1ind  14654  opfi1ind  14657  ccatws1ls  14781  swrdrlen  14809  pfxpfxid  14858  pfxcctswrd  14859  2cshwid  14965  caubnd  15526  dvdsmul1  16447  dvdsmul2  16448  hashbcval  17180  setsvalg  17344  ressval  17411  restval  17597  mrelatglb0  18735  imasmgm2  18863  imasmnd2  18968  efmndov  19077  qusinv  19405  ghminv  19437  gsmsymgrfixlem1  19641  gsmsymgreqlem2  19645  gexod  19800  lsmvalx  19853  rngrz  20388  imasring  20560  irredneg  20660  01eq0ring  20781  ocvin  21980  frlmiscvec  22155  evlrhm  22410  gsumsmonply1  22625  mat1mhm  22799  marrepfval  22875  marrepval0  22876  marepvfval  22880  marepvval0  22881  1elcpmat  23033  m2cpminv0  23079  idpm2idmp  23119  chfacfscmulgsum  23178  chfacfpmmulgsum  23182  restin  23484  qtopval  24014  elqtop3  24022  elfm3  24269  flimval  24282  nmge0  24936  nmeq0  24937  nminv  24940  nmo0  25054  0nghm  25060  coemulhi  26573  isosctrlem2  27147  divsqrtsumlem  27307  2lgsoddprmlem4  27742  0uhgrrusgr  30159  frgruhgr0v  30865  nvge0  31275  nvnd  31290  dip0r  31319  dip0l  31320  nmoo0  31393  hi2eq  31707  wrdsplex  33503  resvval  33890  unitdivcld  34533  signspval  35181  satfv0  36123  ltflcei  38532  elghomlem1OLD  38820  rngorz  38858  rngonegmn1l  38876  rngonegmn1r  38877  igenval  38996  xrnidresex  39363  xrncnvepresex  39364  lfl0  40123  olj01  40283  olm11  40285  hl2at  40463  pmapeq0  40824  trlcl  41222  trlle  41242  tendoid  41831  tendo0plr  41850  tendoipl2  41856  erngmul  41864  erngmul-rN  41872  dvamulr  42070  dvavadd  42073  dvhmulr  42144  cdlemm10N  42176  repncan3  43435  pellfund14  43905  mendmulr  44186  onnoxpg  44430  fmuldfeq  46595  stoweidlem19  47029  stoweidlem26  47036  addsubeq0  48366  zp1modne  48422  modm1nep1  48441  prelspr  48568  lincval1  49531