Theorem mp3an12 1453

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 1450	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 690	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ∧ 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:  mp3an12i  1467  ceqsalg  3501  brelrn  5927  predeq3  6299  funpr  6597  fvpr1  7189  fvpr2  7190  tfi  7853  peano5  7894  wrecseq3  8324  wfr3OLD  8357  fpm  8894  0fsupp  9407  ssttrcl  9734  ac6  10499  alephadd  10596  axpre-sup  11188  cnegex2  11422  addlid  11423  renegcli  11549  div0OLD  11935  divclzi  11981  divcan1zi  11982  divcan2zi  11983  divreczi  11984  divcan3zi  11985  divcan4zi  11986  divasszi  11996  divmulzi  11997  divdirzi  11998  redivclzi  12012  ltm1  12088  mulgt1OLD  12105  recgt1i  12144  ltmul1i  12165  ltdiv1i  12166  ltmuldivi  12167  ltmul2i  12168  lemul1i  12169  lemul2i  12170  ledivp1i  12172  ltdivp1i  12173  nnge1  12273  nngt0  12276  nnrecgt0  12288  nnunb  12502  recnz  12673  eluzsubi  12890  ge0gtmnf  13193  x2times  13320  xrub  13333  xrge0neqmnf  13474  1mod  13925  m1expcl2  14108  1exp  14114  expubnd  14201  iexpcyc  14230  expnbnd  14255  expnlbnd  14256  faclbnd4lem1  14316  imval2  15175  cjdivi  15215  resqrex  15274  sqrtneglem  15290  absdivzi  15431  climcndslem1  15870  climcndslem2  15871  fprodge1  16016  bpoly3  16079  sinhval  16177  coshval  16178  ef01bndlem  16207  sin01gt0  16213  cos01gt0  16214  evend2  16381  divalglem5  16421  vdwlem13  17018  prmlem1  17132  prmlem2  17144  ress0  17269  frmdplusg  18837  m1expaddsub  19484  islindf4  21803  resstopn  23129  lecldbas  23162  hmphindis  23740  cnbl0  24717  xrsmopn  24757  zdis  24761  xrhmeo  24900  oprpiece1res1  24905  voliunlem3  25510  volsup  25514  volivth  25565  iblss2  25764  itgss  25770  coeidp  26226  dgrsub  26235  abelth  26408  reeff1olem  26413  sincosq1sgn  26464  sincosq3sgn  26466  sincosq4sgn  26467  sineq0  26490  logdivlt  26587  1cxp  26638  ecxp  26639  sinasin  26856  log2cnv  26911  efexple  27249  bposlem8  27259  lgsdir2lem2  27294  2sqb  27400  eqscut2  27775  scutun12  27779  eucliddivs  28322  pw2cut  28392  zs12bday  28400  axpaschlem  28924  axlowdimlem9  28934  axlowdimlem12  28937  axlowdimlem16  28941  axlowdimlem17  28942  sizusglecusg  29448  clwlkclwwlkf  29994  imsmetlem  30676  nmoubi  30758  nmobndi  30761  nmounbi  30762  nmlno0lem  30779  nmlnoubi  30782  isblo3i  30787  blometi  30789  blocni  30791  blocn2  30794  ipasslem2  30818  siii  30839  ubthlem1  30856  ubthlem2  30857  ubthlem3  30858  htthlem  30903  hvsubid  31012  hv2times  31047  hi01  31082  hhssabloilem  31247  pjsumi  31696  mayete3i  31714  hoaddcomi  31758  hodsi  31761  hoaddassi  31762  hocadddiri  31765  hocsubdiri  31766  hoaddridi  31772  honegsubi  31782  honegneg  31792  ho2times  31805  eigrei  31820  eigorthi  31823  nmopnegi  31951  hoddii  31975  lnophsi  31987  lnopeqi  31994  nmoptrii  32080  opsqrlem1  32126  opsqrlem6  32131  pjsdii  32141  pjddii  32142  pjscji  32156  pjssposi  32158  pjssdif2i  32160  pjtoi  32165  mdsl2bi  32309  cvmdi  32310  mdslmd3i  32318  mdslmd4i  32319  mdexchi  32321  cvati  32352  cvexchlem  32354  mdsymi  32397  dmdbr5ati  32408  cdj1i  32419  cdj3lem1  32420  xrge0infss  32742  xrge0tsmsd  33061  elrspunidl  33448  2sqr3nconstr  33820  rrhre  34057  esumpinfval  34109  oms0  34334  eulerpartlems  34397  eulerpartlemgf  34416  probmeasb  34467  acycgr2v  35177  cvmliftlem5  35316  bcneg1  35758  wsuceq3  35840  fullfunfv  35970  finminlem  36341  nn0prpwlem  36345  bj-ceqsalg0  36911  bj-ceqsalgALT  36913  bj-ceqsalgvALT  36915  bj-vtoclgfALT  37082  finxpreclem4  37417  sin2h  37639  cos2h  37640  tan2h  37641  poimirlem1  37650  poimirlem2  37651  poimirlem3  37652  poimirlem4  37653  poimirlem6  37655  poimirlem7  37656  poimirlem11  37660  poimirlem12  37661  poimirlem16  37665  poimirlem17  37666  poimirlem19  37668  poimirlem20  37669  poimirlem23  37672  poimirlem30  37679  poimirlem32  37681  poimir  37682  broucube  37683  mblfinlem1  37686  mblfinlem3  37688  mblfinlem4  37689  ismblfin  37690  volsupnfl  37694  iblmulc2nc  37714  ftc1anc  37730  dvasin  37733  heiborlem3  37842  heiborlem6  37845  heiborlem8  37847  cdleme32fva  40461  isnumbasgrplem1  43100  areaquad  43215  binomcxplemnotnn0  44355  permaxun  45011  fourierdlem101  46216  fourierdlem103  46218  fourierdlem104  46219  sqwvfourb  46238  fourierswlem  46239  fouriersw  46240  m1mod0mod1  47363  sgoldbeven3prm  47777  iooii  48872  aacllem  49645