Theorem mp3an12 1480

Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)

Hypotheses

Ref	Expression
mp3an12.1	⊢ 𝜑
mp3an12.2	⊢ 𝜓
mp3an12.3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an12	⊢ (𝜒 → 𝜃)

Proof of Theorem mp3an12

Step	Hyp	Ref	Expression
1		mp3an12.2	. 2 ⊢ 𝜓
2		mp3an12.1	. . 3 ⊢ 𝜑
3		mp3an12.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	mp3an1 1477	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 703	1 ⊢ (𝜒 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mp3an12i  1494  ceqsalg  3488  brelrn  5930  predeq3  6307  funpr  6593  fvpr1  7193  fvpr2  7194  tfi  7852  peano5  7893  wrecseq3  8319  fpm  8885  0fsupp  9363  ssttrcl  9697  ac6  10485  alephadd  10589  axpre-sup  11181  cnegex2  11419  addlid  11420  renegcli  11546  divclzi  11977  divcan1zi  11978  divcan2zi  11979  divreczi  11980  divcan3zi  11981  divcan4zi  11982  divasszi  11992  divmulzi  11993  divdirzi  11994  redivclzi  12008  ltm1  12084  recgt1i  12139  ltmul1i  12160  ltdiv1i  12161  ltmuldivi  12162  ltmul2i  12163  lemul1i  12164  lemul2i  12165  ledivp1i  12167  ltdivp1i  12168  nnge1  12291  nngt0  12294  nnrecgt0  12306  nnunb  12527  recnz  12699  eluzsubi  12922  ge0gtmnf  13226  x2times  13353  xrub  13366  xrge0neqmnf  13507  1mod  13966  m1expcl2  14151  1exp  14157  expubnd  14244  iexpcyc  14273  expnbnd  14298  expnlbnd  14299  faclbnd4lem1  14359  imval2  15240  cjdivi  15280  resqrex  15339  sqrtneglem  15355  absdivzi  15497  climcndslem1  15940  climcndslem2  15941  fprodge1  16086  bpoly3  16148  sinhval  16246  coshval  16247  ef01bndlem  16276  sin01gt0  16282  cos01gt0  16283  evend2  16451  divalglem5  16491  vdwlem13  17089  prmlem1  17203  prmlem2  17216  ress0  17339  frmdplusg  18964  m1expaddsub  19626  islindf4  22052  resstopn  23412  lecldbas  23445  hmphindis  24024  cnbl0  25000  xrsmopn  25040  zdis  25044  xrhmeo  25175  oprpiece1res1  25180  voliunlem3  25781  volsup  25785  volivth  25836  iblss2  26035  itgss  26041  coeidp  26490  dgrsub  26499  abelth  26674  reeff1olem  26679  sincosq1sgn  26733  sincosq3sgn  26735  sincosq4sgn  26736  sineq0  26759  logdivlt  26856  1cxp  26907  ecxp  26908  sinasin  27124  log2cnv  27179  efexple  27515  bposlem8  27525  lgsdir2lem2  27560  2sqb  27666  eqcuts2  28049  cutsun12  28053  eucliddivs  28639  pw2cut  28723  axpaschlem  29383  axlowdimlem9  29393  axlowdimlem12  29396  axlowdimlem16  29400  axlowdimlem17  29401  sizusglecusg  29909  clwlkclwwlkf  30464  imsmetlem  31157  nmoubi  31239  nmobndi  31242  nmounbi  31243  nmlno0lem  31260  nmlnoubi  31263  isblo3i  31268  blometi  31270  blocni  31272  blocn2  31275  ipasslem2  31299  siii  31320  ubthlem1  31337  ubthlem2  31338  ubthlem3  31339  htthlem  31384  hvsubid  31493  hv2times  31528  hi01  31563  hhssabloilem  31728  pjsumi  32177  mayete3i  32195  hoaddcomi  32239  hodsi  32242  hoaddassi  32243  hocadddiri  32246  hocsubdiri  32247  hoaddridi  32253  honegsubi  32263  honegneg  32273  ho2times  32286  eigrei  32301  eigorthi  32304  nmopnegi  32432  hoddii  32456  lnophsi  32468  lnopeqi  32475  nmoptrii  32561  opsqrlem1  32607  opsqrlem6  32612  pjsdii  32622  pjddii  32623  pjscji  32637  pjssposi  32639  pjssdif2i  32641  pjtoi  32646  mdsl2bi  32790  cvmdi  32791  mdslmd3i  32799  mdslmd4i  32800  mdexchi  32802  cvati  32833  cvexchlem  32835  mdsymi  32878  dmdbr5ati  32889  cdj1i  32900  cdj3lem1  32901  xrge0infss  33218  xrge0tsmsd  33500  elrspunidl  33843  2sqr3nconstr  34278  cos9thpinconstrlem2  34287  rrhre  34518  esumpinfval  34570  oms0  34795  eulerpartlems  34858  eulerpartlemgf  34877  probmeasb  34928  dfscott2  35612  dfscott3  35613  acycgr2v  35716  cvmliftlem5  35855  bcneg1  36302  wsuceq3  36381  fullfunfv  36513  finminlem  36924  nn0prpwlem  36928  regsfromunir1  37146  bj-ceqsalg0  37618  bj-ceqsalgALT  37620  bj-ceqsalgvALT  37622  bj-vtoclgfALT  37790  finxpreclem4  38135  sin2h  38351  cos2h  38352  tan2h  38353  poimirlem1  38357  poimirlem2  38358  poimirlem3  38359  poimirlem4  38360  poimirlem6  38362  poimirlem7  38363  poimirlem11  38367  poimirlem12  38368  poimirlem16  38372  poimirlem17  38373  poimirlem19  38375  poimirlem20  38376  poimirlem23  38379  poimirlem30  38386  poimirlem32  38388  poimir  38389  broucube  38390  mblfinlem1  38393  mblfinlem3  38395  mblfinlem4  38396  ismblfin  38397  volsupnfl  38401  iblmulc2nc  38421  ftc1anc  38437  dvasin  38440  heiborlem3  38550  heiborlem6  38553  heiborlem8  38555  cdleme32fva  41297  isnumbasgrplem1  43929  areaquad  44044  binomcxplemnotnn0  45167  permaxun  45821  fourierdlem101  47022  fourierdlem103  47024  fourierdlem104  47025  sqwvfourb  47044  fourierswlem  47045  fouriersw  47046  m1mod0mod1  48235  sgoldbeven3prm  48686  pgnbgreunbgrlem2lem1  49017  pgnbgreunbgrlem2lem2  49018  pgnbgreunbgrlem2lem3  49019  iooii  49831  aacllem  50759