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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  stoic2b  1777  elovmpo  7605  f1oeng  8910  php  9134  nnsdomg  9202  wdomimag  9495  gruuni  10714  genpv  10913  pncan3  11392  mulsubaddmulsub  11605  infssuzle  12872  fzrevral3  13559  flflp1  13757  subsq2  14164  brfi1ind  14462  opfi1ind  14465  ccatws1ls  14587  swrdrlen  14613  pfxpfxid  14662  pfxcctswrd  14663  2cshwid  14767  caubnd  15312  dvdsmul1  16237  dvdsmul2  16238  hashbcval  16964  setsvalg  17127  ressval  17194  restval  17380  mrelatglb0  18518  imasmnd2  18733  efmndov  18840  qusinv  19156  ghminv  19189  gsmsymgrfixlem1  19393  gsmsymgreqlem2  19397  gexod  19552  lsmvalx  19605  rngrz  20138  imasring  20301  irredneg  20401  01eq0ring  20498  ocvin  21664  frlmiscvec  21839  evlrhm  22089  gsumsmonply1  22282  mat1mhm  22459  marrepfval  22535  marrepval0  22536  marepvfval  22540  marepvval0  22541  1elcpmat  22690  m2cpminv0  22736  idpm2idmp  22776  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  restin  23141  qtopval  23670  elqtop3  23678  elfm3  23925  flimval  23938  nmge0  24592  nmeq0  24593  nminv  24596  nmo0  24710  0nghm  24716  coemulhi  26229  isosctrlem2  26796  divsqrtsumlem  26957  2lgsoddprmlem4  27392  0uhgrrusgr  29662  frgruhgr0v  30349  nvge0  30759  nvnd  30774  dip0r  30803  dip0l  30804  nmoo0  30877  hi2eq  31191  wrdsplex  33011  resvval  33404  unitdivcld  34061  signspval  34712  satfv0  35556  ltflcei  37943  elghomlem1OLD  38220  rngorz  38258  rngonegmn1l  38276  rngonegmn1r  38277  igenval  38396  xrnidresex  38765  xrncnvepresex  38766  lfl0  39525  olj01  39685  olm11  39687  hl2at  39865  pmapeq0  40226  trlcl  40624  trlle  40644  tendoid  41233  tendo0plr  41252  tendoipl2  41258  erngmul  41266  erngmul-rN  41274  dvamulr  41472  dvavadd  41475  dvhmulr  41546  cdlemm10N  41578  repncan3  42829  pellfund14  43344  mendmulr  43630  onnoxpg  43874  fmuldfeq  46031  stoweidlem19  46465  stoweidlem26  46472  addsubeq0  47756  zp1modne  47812  modm1nep1  47831  prelspr  47958  lincval1  48907