Theorem mpd3an3 1461

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 1117	. 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  1771  elovmpo  7677  f1oeng  9009  php  9244  nnsdomg  9332  wdomimag  9624  gruuni  10837  genpv  11036  pncan3  11513  mulsubaddmulsub  11724  infssuzle  12970  fzrevral3  13650  flflp1  13843  subsq2  14246  brfi1ind  14544  opfi1ind  14547  ccatws1ls  14667  swrdrlen  14693  pfxpfxid  14743  pfxcctswrd  14744  2cshwid  14848  caubnd  15393  dvdsmul1  16311  dvdsmul2  16312  hashbcval  17035  setsvalg  17199  ressval  17276  restval  17472  mrelatglb0  18618  imasmnd2  18799  efmndov  18906  qusinv  19220  ghminv  19253  gsmsymgrfixlem1  19459  gsmsymgreqlem2  19463  gexod  19618  lsmvalx  19671  rngrz  20183  imasring  20343  irredneg  20446  01eq0ring  20546  ocvin  21709  frlmiscvec  21886  evlrhm  22137  gsumsmonply1  22326  mat1mhm  22505  marrepfval  22581  marrepval0  22582  marepvfval  22586  marepvval0  22587  1elcpmat  22736  m2cpminv0  22782  idpm2idmp  22822  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  restin  23189  qtopval  23718  elqtop3  23726  elfm3  23973  flimval  23986  nmge0  24645  nmeq0  24646  nminv  24649  nmo0  24771  0nghm  24777  coemulhi  26307  isosctrlem2  26876  divsqrtsumlem  27037  2lgsoddprmlem4  27473  0uhgrrusgr  29610  frgruhgr0v  30292  nvge0  30701  nvnd  30716  dip0r  30745  dip0l  30746  nmoo0  30819  hi2eq  31133  wrdsplex  32904  resvval  33332  unitdivcld  33861  signspval  34545  satfv0  35342  ltflcei  37594  elghomlem1OLD  37871  rngorz  37909  rngonegmn1l  37927  rngonegmn1r  37928  igenval  38047  xrnidresex  38388  xrncnvepresex  38389  lfl0  39046  olj01  39206  olm11  39208  hl2at  39387  pmapeq0  39748  trlcl  40146  trlle  40166  tendoid  40755  tendo0plr  40774  tendoipl2  40780  erngmul  40788  erngmul-rN  40796  dvamulr  40994  dvavadd  40997  dvhmulr  41068  cdlemm10N  41100  repncan3  42389  pellfund14  42885  mendmulr  43172  onnog  43418  fmuldfeq  45538  stoweidlem19  45974  stoweidlem26  45981  addsubeq0  47245  zp1modne  47285  prelspr  47410  lincval1  48264