Theorem mpd3an3 1462

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 685	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  stoic2b  1777  elovmpo  7647  f1oeng  8963  php  9206  nnsdomg  9298  wdomimag  9578  gruuni  10791  genpv  10990  pncan3  11464  mulsubaddmulsub  11674  infssuzle  12911  fzrevral3  13584  flflp1  13768  subsq2  14171  brfi1ind  14456  opfi1ind  14459  ccatws1ls  14579  swrdrlen  14605  pfxpfxid  14655  pfxcctswrd  14656  2cshwid  14760  caubnd  15301  dvdsmul1  16217  dvdsmul2  16218  hashbcval  16931  setsvalg  17095  ressval  17172  restval  17368  mrelatglb0  18510  imasmnd2  18658  efmndov  18758  qusinv  19063  ghminv  19093  gsmsymgrfixlem1  19289  gsmsymgreqlem2  19293  gexod  19448  lsmvalx  19501  ringrz  20101  imasring  20136  irredneg  20236  01eq0ring  20297  ocvin  21218  frlmiscvec  21395  evlrhm  21650  gsumsmonply1  21818  mat1mhm  21977  marrepfval  22053  marrepval0  22054  marepvfval  22058  marepvval0  22059  1elcpmat  22208  m2cpminv0  22254  idpm2idmp  22294  chfacfscmulgsum  22353  chfacfpmmulgsum  22357  restin  22661  qtopval  23190  elqtop3  23198  elfm3  23445  flimval  23458  nmge0  24117  nmeq0  24118  nminv  24121  nmo0  24243  0nghm  24249  coemulhi  25759  isosctrlem2  26313  divsqrtsumlem  26473  2lgsoddprmlem4  26907  0uhgrrusgr  28824  frgruhgr0v  29506  nvge0  29913  nvnd  29928  dip0r  29957  dip0l  29958  nmoo0  30031  hi2eq  30345  wrdsplex  32091  resvval  32429  unitdivcld  32869  signspval  33551  satfv0  34337  ovmul  35148  ltflcei  36464  elghomlem1OLD  36741  rngorz  36779  rngonegmn1l  36797  rngonegmn1r  36798  igenval  36917  xrnidresex  37265  xrncnvepresex  37266  lfl0  37923  olj01  38083  olm11  38085  hl2at  38264  pmapeq0  38625  trlcl  39023  trlle  39043  tendoid  39632  tendo0plr  39651  tendoipl2  39657  erngmul  39665  erngmul-rN  39673  dvamulr  39871  dvavadd  39874  dvhmulr  39945  cdlemm10N  39977  repncan3  41252  pellfund14  41621  mendmulr  41915  onnog  42165  fmuldfeq  44285  stoweidlem19  44721  stoweidlem26  44728  addsubeq0  45990  prelspr  46140  rngrz  46651  lincval1  47053