Theorem mp3an12 1454

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  mp3an12i  1468  ceqsalg  3477  brelrn  5892  predeq3  6264  funpr  6549  fvpr1  7141  fvpr2  7142  tfi  7798  peano5  7838  wrecseq3  8262  fpm  8818  0fsupp  9298  ssttrcl  9629  ac6  10395  alephadd  10493  axpre-sup  11085  cnegex2  11320  addlid  11321  renegcli  11447  div0OLD  11835  divclzi  11881  divcan1zi  11882  divcan2zi  11883  divreczi  11884  divcan3zi  11885  divcan4zi  11886  divasszi  11896  divmulzi  11897  divdirzi  11898  redivclzi  11912  ltm1  11988  mulgt1OLD  12005  recgt1i  12044  ltmul1i  12065  ltdiv1i  12066  ltmuldivi  12067  ltmul2i  12068  lemul1i  12069  lemul2i  12070  ledivp1i  12072  ltdivp1i  12073  nnge1  12178  nngt0  12181  nnrecgt0  12193  nnunb  12402  recnz  12572  eluzsubi  12788  ge0gtmnf  13092  x2times  13219  xrub  13232  xrge0neqmnf  13373  1mod  13828  m1expcl2  14013  1exp  14019  expubnd  14106  iexpcyc  14135  expnbnd  14160  expnlbnd  14161  faclbnd4lem1  14221  imval2  15079  cjdivi  15119  resqrex  15178  sqrtneglem  15194  absdivzi  15336  climcndslem1  15777  climcndslem2  15778  fprodge1  15923  bpoly3  15986  sinhval  16084  coshval  16085  ef01bndlem  16114  sin01gt0  16120  cos01gt0  16121  evend2  16289  divalglem5  16329  vdwlem13  16926  prmlem1  17040  prmlem2  17052  ress0  17175  frmdplusg  18784  m1expaddsub  19432  islindf4  21798  resstopn  23135  lecldbas  23168  hmphindis  23746  cnbl0  24722  xrsmopn  24762  zdis  24766  xrhmeo  24905  oprpiece1res1  24910  voliunlem3  25514  volsup  25518  volivth  25569  iblss2  25768  itgss  25774  coeidp  26230  dgrsub  26239  abelth  26412  reeff1olem  26417  sincosq1sgn  26468  sincosq3sgn  26470  sincosq4sgn  26471  sineq0  26494  logdivlt  26591  1cxp  26642  ecxp  26643  sinasin  26860  log2cnv  26915  efexple  27253  bposlem8  27263  lgsdir2lem2  27298  2sqb  27404  eqcuts2  27787  cutsun12  27791  eucliddivs  28377  pw2cut  28461  axpaschlem  29018  axlowdimlem9  29028  axlowdimlem12  29031  axlowdimlem16  29035  axlowdimlem17  29036  sizusglecusg  29542  clwlkclwwlkf  30088  imsmetlem  30770  nmoubi  30852  nmobndi  30855  nmounbi  30856  nmlno0lem  30873  nmlnoubi  30876  isblo3i  30881  blometi  30883  blocni  30885  blocn2  30888  ipasslem2  30912  siii  30933  ubthlem1  30950  ubthlem2  30951  ubthlem3  30952  htthlem  30997  hvsubid  31106  hv2times  31141  hi01  31176  hhssabloilem  31341  pjsumi  31790  mayete3i  31808  hoaddcomi  31852  hodsi  31855  hoaddassi  31856  hocadddiri  31859  hocsubdiri  31860  hoaddridi  31866  honegsubi  31876  honegneg  31886  ho2times  31899  eigrei  31914  eigorthi  31917  nmopnegi  32045  hoddii  32069  lnophsi  32081  lnopeqi  32088  nmoptrii  32174  opsqrlem1  32220  opsqrlem6  32225  pjsdii  32235  pjddii  32236  pjscji  32250  pjssposi  32252  pjssdif2i  32254  pjtoi  32259  mdsl2bi  32403  cvmdi  32404  mdslmd3i  32412  mdslmd4i  32413  mdexchi  32415  cvati  32446  cvexchlem  32448  mdsymi  32491  dmdbr5ati  32502  cdj1i  32513  cdj3lem1  32514  xrge0infss  32843  xrge0tsmsd  33159  elrspunidl  33513  2sqr3nconstr  33951  cos9thpinconstrlem2  33960  rrhre  34191  esumpinfval  34243  oms0  34467  eulerpartlems  34530  eulerpartlemgf  34549  probmeasb  34600  acycgr2v  35357  cvmliftlem5  35496  bcneg1  35943  wsuceq3  36022  fullfunfv  36154  finminlem  36525  nn0prpwlem  36529  regsfromunir1  36683  bj-ceqsalg0  37102  bj-ceqsalgALT  37104  bj-ceqsalgvALT  37106  bj-vtoclgfALT  37273  finxpreclem4  37612  sin2h  37824  cos2h  37825  tan2h  37826  poimirlem1  37835  poimirlem2  37836  poimirlem3  37837  poimirlem4  37838  poimirlem6  37840  poimirlem7  37841  poimirlem11  37845  poimirlem12  37846  poimirlem16  37850  poimirlem17  37851  poimirlem19  37853  poimirlem20  37854  poimirlem23  37857  poimirlem30  37864  poimirlem32  37866  poimir  37867  broucube  37868  mblfinlem1  37871  mblfinlem3  37873  mblfinlem4  37874  ismblfin  37875  volsupnfl  37879  iblmulc2nc  37899  ftc1anc  37915  dvasin  37918  heiborlem3  38027  heiborlem6  38030  heiborlem8  38032  cdleme32fva  40776  isnumbasgrplem1  43421  areaquad  43536  binomcxplemnotnn0  44675  permaxun  45330  fourierdlem101  46528  fourierdlem103  46530  fourierdlem104  46531  sqwvfourb  46550  fourierswlem  46551  fouriersw  46552  m1mod0mod1  47677  sgoldbeven3prm  48106  pgnbgreunbgrlem2lem1  48437  pgnbgreunbgrlem2lem2  48438  pgnbgreunbgrlem2lem3  48439  iooii  49240  aacllem  50123