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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  stoic2b  1740  elovmpt2  6921  f1oeng  8016  wdomimag  8533  cdaval  9030  gruuni  9660  genpv  9859  infssuzle  11809  fzrevral3  12465  flflp1  12648  subsq2  13013  brfi1ind  13319  opfi1ind  13322  ccatws1ls  13455  swrdrlen  13481  swrd0swrdid  13510  2cshwid  13606  caubnd  14142  dvdsmul1  15050  dvdsmul2  15051  hashbcval  15753  setsvalg  15934  ressval  15974  restval  16134  mrelatglb0  17232  imasmnd2  17374  qusinv  17700  ghminv  17714  symgov  17856  gexod  18047  lsmvalx  18100  ringrz  18634  imasring  18665  irredneg  18756  evlrhm  19573  gsumsmonply1  19721  ocvin  20066  frlmiscvec  20236  mat1mhm  20338  marrepfval  20414  marrepval0  20415  marepvfval  20419  marepvval0  20420  1elcpmat  20568  m2cpminv0  20614  idpm2idmp  20654  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  restin  21018  qtopval  21546  elqtop3  21554  elfm3  21801  flimval  21814  nmge0  22468  nmeq0  22469  nminv  22472  nmo0  22586  0nghm  22592  coemulhi  24055  isosctrlem2  24594  divsqrtsumlem  24751  2lgsoddprmlem4  25185  0uhgrrusgr  26530  frgruhgr0v  27243  nvge0  27656  nvnd  27671  dip0r  27700  dip0l  27701  nmoo0  27774  hi2eq  28090  resvval  29955  unitdivcld  30075  signspval  30757  ltflcei  33527  elghomlem1OLD  33814  rngorz  33852  rngonegmn1l  33870  rngonegmn1r  33871  igenval  33990  xrnidresex  34305  xrncnvepresex  34306  lfl0  34670  olj01  34830  olm11  34832  hl2at  35009  pmapeq0  35370  trlcl  35769  trlle  35789  tendoid  36378  tendo0plr  36397  tendoipl2  36403  erngmul  36411  erngmul-rN  36419  dvamulr  36617  dvavadd  36620  dvhmulr  36692  cdlemm10N  36724  pellfund14  37779  mendmulr  38075  fmuldfeq  40133  stoweidlem19  40554  stoweidlem26  40561  pfxpfxid  41741  pfxcctswrd  41742  prelspr  42061  lincval1  42533