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  9000  php  9225  nnsdomg  9294  wdomimag  9584  gruuni  10888  genpv  11087  pncan3  11568  mulsubaddmulsub  11783  infssuzle  13061  fzrevral3  13751  flflp1  13950  subsq2  14358  brfi1ind  14657  opfi1ind  14660  ccatws1ls  14785  swrdrlen  14813  pfxpfxid  14862  pfxcctswrd  14863  2cshwid  14969  caubnd  15531  dvdsmul1  16452  dvdsmul2  16453  hashbcval  17185  setsvalg  17349  ressval  17416  restval  17602  mrelatglb0  18740  imasmgm2  18868  imasmnd2  18973  efmndov  19082  qusinv  19410  ghminv  19442  gsmsymgrfixlem1  19646  gsmsymgreqlem2  19650  gexod  19805  lsmvalx  19858  rngrz  20393  imasring  20565  irredneg  20665  01eq0ring  20786  ocvin  21985  frlmiscvec  22160  evlrhm  22415  gsumsmonply1  22630  mat1mhm  22804  marrepfval  22880  marrepval0  22881  marepvfval  22885  marepvval0  22886  1elcpmat  23038  m2cpminv0  23084  idpm2idmp  23124  chfacfscmulgsum  23183  chfacfpmmulgsum  23187  restin  23489  qtopval  24019  elqtop3  24027  elfm3  24274  flimval  24287  nmge0  24941  nmeq0  24942  nminv  24945  nmo0  25059  0nghm  25065  coemulhi  26578  isosctrlem2  27152  divsqrtsumlem  27312  2lgsoddprmlem4  27747  0uhgrrusgr  30164  frgruhgr0v  30870  nvge0  31280  nvnd  31295  dip0r  31324  dip0l  31325  nmoo0  31398  hi2eq  31712  wrdsplex  33549  resvval  33936  unitdivcld  34579  signspval  35227  satfv0  36209  ltflcei  38624  elghomlem1OLD  38912  rngorz  38950  rngonegmn1l  38968  rngonegmn1r  38969  igenval  39088  xrnidresex  39455  xrncnvepresex  39456  lfl0  40215  olj01  40375  olm11  40377  hl2at  40555  pmapeq0  40916  trlcl  41314  trlle  41334  tendoid  41923  tendo0plr  41942  tendoipl2  41948  erngmul  41956  erngmul-rN  41964  dvamulr  42162  dvavadd  42165  dvhmulr  42236  cdlemm10N  42268  repncan3  43527  pellfund14  43998  mendmulr  44279  onnoxpg  44523  fmuldfeq  46688  stoweidlem19  47122  stoweidlem26  47129  addsubeq0  48459  zp1modne  48515  modm1nep1  48534  prelspr  48661  lincval1  49624