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  7591  f1oeng  8893  php  9116  nnsdomg  9183  wdomimag  9473  gruuni  10688  genpv  10887  pncan3  11365  mulsubaddmulsub  11578  infssuzle  12826  fzrevral3  13511  flflp1  13708  subsq2  14115  brfi1ind  14413  opfi1ind  14416  ccatws1ls  14538  swrdrlen  14564  pfxpfxid  14613  pfxcctswrd  14614  2cshwid  14718  caubnd  15263  dvdsmul1  16185  dvdsmul2  16186  hashbcval  16911  setsvalg  17074  ressval  17141  restval  17327  mrelatglb0  18464  imasmnd2  18679  efmndov  18786  qusinv  19100  ghminv  19133  gsmsymgrfixlem1  19337  gsmsymgreqlem2  19341  gexod  19496  lsmvalx  19549  rngrz  20082  imasring  20246  irredneg  20346  01eq0ring  20443  ocvin  21609  frlmiscvec  21784  evlrhm  22029  gsumsmonply1  22220  mat1mhm  22397  marrepfval  22473  marrepval0  22474  marepvfval  22478  marepvval0  22479  1elcpmat  22628  m2cpminv0  22674  idpm2idmp  22714  chfacfscmulgsum  22773  chfacfpmmulgsum  22777  restin  23079  qtopval  23608  elqtop3  23616  elfm3  23863  flimval  23876  nmge0  24530  nmeq0  24531  nminv  24534  nmo0  24648  0nghm  24654  coemulhi  26184  isosctrlem2  26754  divsqrtsumlem  26915  2lgsoddprmlem4  27351  0uhgrrusgr  29555  frgruhgr0v  30239  nvge0  30648  nvnd  30663  dip0r  30692  dip0l  30693  nmoo0  30766  hi2eq  31080  wrdsplex  32912  resvval  33289  unitdivcld  33909  signspval  34560  satfv0  35390  ltflcei  37647  elghomlem1OLD  37924  rngorz  37962  rngonegmn1l  37980  rngonegmn1r  37981  igenval  38100  xrnidresex  38438  xrncnvepresex  38439  lfl0  39103  olj01  39263  olm11  39265  hl2at  39443  pmapeq0  39804  trlcl  40202  trlle  40222  tendoid  40811  tendo0plr  40830  tendoipl2  40836  erngmul  40844  erngmul-rN  40852  dvamulr  41050  dvavadd  41053  dvhmulr  41124  cdlemm10N  41156  repncan3  42415  pellfund14  42930  mendmulr  43216  onnog  43461  fmuldfeq  45622  stoweidlem19  46056  stoweidlem26  46063  addsubeq0  47326  zp1modne  47376  modm1nep1  47395  prelspr  47516  lincval1  48450