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  7597  f1oeng  8899  php  9123  nnsdomg  9190  wdomimag  9480  gruuni  10698  genpv  10897  pncan3  11375  mulsubaddmulsub  11588  infssuzle  12831  fzrevral3  13516  flflp1  13713  subsq2  14120  brfi1ind  14418  opfi1ind  14421  ccatws1ls  14543  swrdrlen  14569  pfxpfxid  14618  pfxcctswrd  14619  2cshwid  14723  caubnd  15268  dvdsmul1  16190  dvdsmul2  16191  hashbcval  16916  setsvalg  17079  ressval  17146  restval  17332  mrelatglb0  18469  imasmnd2  18684  efmndov  18791  qusinv  19104  ghminv  19137  gsmsymgrfixlem1  19341  gsmsymgreqlem2  19345  gexod  19500  lsmvalx  19553  rngrz  20086  imasring  20250  irredneg  20350  01eq0ring  20447  ocvin  21613  frlmiscvec  21788  evlrhm  22032  gsumsmonply1  22223  mat1mhm  22400  marrepfval  22476  marrepval0  22477  marepvfval  22481  marepvval0  22482  1elcpmat  22631  m2cpminv0  22677  idpm2idmp  22717  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  restin  23082  qtopval  23611  elqtop3  23619  elfm3  23866  flimval  23879  nmge0  24533  nmeq0  24534  nminv  24537  nmo0  24651  0nghm  24657  coemulhi  26187  isosctrlem2  26757  divsqrtsumlem  26918  2lgsoddprmlem4  27354  0uhgrrusgr  29559  frgruhgr0v  30246  nvge0  30655  nvnd  30670  dip0r  30699  dip0l  30700  nmoo0  30773  hi2eq  31087  wrdsplex  32924  resvval  33301  unitdivcld  33935  signspval  34586  satfv0  35423  ltflcei  37668  elghomlem1OLD  37945  rngorz  37983  rngonegmn1l  38001  rngonegmn1r  38002  igenval  38121  xrnidresex  38474  xrncnvepresex  38475  lfl0  39184  olj01  39344  olm11  39346  hl2at  39524  pmapeq0  39885  trlcl  40283  trlle  40303  tendoid  40892  tendo0plr  40911  tendoipl2  40917  erngmul  40925  erngmul-rN  40933  dvamulr  41131  dvavadd  41134  dvhmulr  41205  cdlemm10N  41237  repncan3  42501  pellfund14  43015  mendmulr  43301  onnog  43546  fmuldfeq  45707  stoweidlem19  46141  stoweidlem26  46148  addsubeq0  47420  zp1modne  47470  modm1nep1  47489  prelspr  47610  lincval1  48544