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  1808  elovmpo  7663  f1oeng  8980  php  9205  nnsdomg  9273  wdomimag  9563  gruuni  10813  genpv  11012  pncan3  11493  mulsubaddmulsub  11706  infssuzle  12984  fzrevral3  13673  flflp1  13872  subsq2  14279  brfi1ind  14578  opfi1ind  14581  ccatws1ls  14705  swrdrlen  14733  pfxpfxid  14782  pfxcctswrd  14783  2cshwid  14889  caubnd  15450  dvdsmul1  16373  dvdsmul2  16374  hashbcval  17100  setsvalg  17264  ressval  17331  restval  17517  mrelatglb0  18655  imasmgm2  18782  imasmnd2  18887  efmndov  18996  qusinv  19324  ghminv  19356  gsmsymgrfixlem1  19560  gsmsymgreqlem2  19564  gexod  19719  lsmvalx  19772  rngrz  20307  imasring  20477  irredneg  20577  01eq0ring  20697  ocvin  21893  frlmiscvec  22068  evlrhm  22323  gsumsmonply1  22538  mat1mhm  22712  marrepfval  22788  marrepval0  22789  marepvfval  22793  marepvval0  22794  1elcpmat  22946  m2cpminv0  22992  idpm2idmp  23032  chfacfscmulgsum  23091  chfacfpmmulgsum  23095  restin  23397  qtopval  23927  elqtop3  23935  elfm3  24182  flimval  24195  nmge0  24849  nmeq0  24850  nminv  24853  nmo0  24967  0nghm  24973  coemulhi  26487  isosctrlem2  27064  divsqrtsumlem  27224  2lgsoddprmlem4  27659  0uhgrrusgr  30046  frgruhgr0v  30752  nvge0  31162  nvnd  31177  dip0r  31206  dip0l  31207  nmoo0  31280  hi2eq  31594  wrdsplex  33390  resvval  33777  unitdivcld  34419  signspval  35068  satfv0  35945  ltflcei  38370  elghomlem1OLD  38643  rngorz  38681  rngonegmn1l  38699  rngonegmn1r  38700  igenval  38819  xrnidresex  39186  xrncnvepresex  39187  lfl0  39946  olj01  40106  olm11  40108  hl2at  40286  pmapeq0  40647  trlcl  41045  trlle  41065  tendoid  41654  tendo0plr  41673  tendoipl2  41679  erngmul  41687  erngmul-rN  41695  dvamulr  41893  dvavadd  41896  dvhmulr  41967  cdlemm10N  41999  repncan3  43266  pellfund14  43747  mendmulr  44033  onnoxpg  44277  fmuldfeq  46421  stoweidlem19  46855  stoweidlem26  46862  addsubeq0  48192  zp1modne  48248  modm1nep1  48267  prelspr  48394  lincval1  49357