Theorem mpd3an3 1464

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  stoic2b  1776  elovmpo  7603  f1oeng  8907  php  9131  nnsdomg  9199  wdomimag  9492  gruuni  10711  genpv  10910  pncan3  11388  mulsubaddmulsub  11601  infssuzle  12844  fzrevral3  13530  flflp1  13727  subsq2  14134  brfi1ind  14432  opfi1ind  14435  ccatws1ls  14557  swrdrlen  14583  pfxpfxid  14632  pfxcctswrd  14633  2cshwid  14737  caubnd  15282  dvdsmul1  16204  dvdsmul2  16205  hashbcval  16930  setsvalg  17093  ressval  17160  restval  17346  mrelatglb0  18484  imasmnd2  18699  efmndov  18806  qusinv  19119  ghminv  19152  gsmsymgrfixlem1  19356  gsmsymgreqlem2  19360  gexod  19515  lsmvalx  19568  rngrz  20101  imasring  20266  irredneg  20366  01eq0ring  20463  ocvin  21629  frlmiscvec  21804  evlrhm  22056  gsumsmonply1  22251  mat1mhm  22428  marrepfval  22504  marrepval0  22505  marepvfval  22509  marepvval0  22510  1elcpmat  22659  m2cpminv0  22705  idpm2idmp  22745  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  restin  23110  qtopval  23639  elqtop3  23647  elfm3  23894  flimval  23907  nmge0  24561  nmeq0  24562  nminv  24565  nmo0  24679  0nghm  24685  coemulhi  26215  isosctrlem2  26785  divsqrtsumlem  26946  2lgsoddprmlem4  27382  0uhgrrusgr  29652  frgruhgr0v  30339  nvge0  30748  nvnd  30763  dip0r  30792  dip0l  30793  nmoo0  30866  hi2eq  31180  wrdsplex  33018  resvval  33410  unitdivcld  34058  signspval  34709  satfv0  35552  ltflcei  37805  elghomlem1OLD  38082  rngorz  38120  rngonegmn1l  38138  rngonegmn1r  38139  igenval  38258  xrnidresex  38611  xrncnvepresex  38612  lfl0  39321  olj01  39481  olm11  39483  hl2at  39661  pmapeq0  40022  trlcl  40420  trlle  40440  tendoid  41029  tendo0plr  41048  tendoipl2  41054  erngmul  41062  erngmul-rN  41070  dvamulr  41268  dvavadd  41271  dvhmulr  41342  cdlemm10N  41374  repncan3  42634  pellfund14  43136  mendmulr  43422  onnoxpg  43666  fmuldfeq  45825  stoweidlem19  46259  stoweidlem26  46266  addsubeq0  47538  zp1modne  47588  modm1nep1  47607  prelspr  47728  lincval1  48661