Theorem mp3an12 1462

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

Syntax hints:   → wi 4   ∧ w3a 1095

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 209  df-an 399  df-3an 1097

This theorem is referenced by:  mp3an12i  1476  ceqsalg  3479  brelrn  5907  predeq3  6277  funpr  6562  fvpr1  7161  fvpr2  7162  tfi  7818  peano5  7859  wrecseq3  8282  fpm  8842  0fsupp  9322  ssttrcl  9656  ac6  10423  alephadd  10521  axpre-sup  11113  cnegex2  11351  addlid  11352  renegcli  11478  div0OLD  11865  divclzi  11912  divcan1zi  11913  divcan2zi  11914  divreczi  11915  divcan3zi  11916  divcan4zi  11917  divasszi  11927  divmulzi  11928  divdirzi  11929  redivclzi  11943  ltm1  12019  mulgt1OLD  12036  recgt1i  12075  ltmul1i  12096  ltdiv1i  12097  ltmuldivi  12098  ltmul2i  12099  lemul1i  12100  lemul2i  12101  ledivp1i  12103  ltdivp1i  12104  nnge1  12227  nngt0  12230  nnrecgt0  12242  nnunb  12463  recnz  12634  eluzsubi  12857  ge0gtmnf  13161  x2times  13288  xrub  13301  xrge0neqmnf  13442  1mod  13899  m1expcl2  14084  1exp  14090  expubnd  14177  iexpcyc  14206  expnbnd  14231  expnlbnd  14232  faclbnd4lem1  14292  imval2  15150  cjdivi  15190  resqrex  15249  sqrtneglem  15265  absdivzi  15407  climcndslem1  15851  climcndslem2  15852  fprodge1  15997  bpoly3  16060  sinhval  16158  coshval  16159  ef01bndlem  16188  sin01gt0  16194  cos01gt0  16195  evend2  16363  divalglem5  16403  vdwlem13  17001  prmlem1  17115  prmlem2  17128  ress0  17251  frmdplusg  18860  m1expaddsub  19510  islindf4  21859  resstopn  23215  lecldbas  23248  hmphindis  23826  cnbl0  24802  xrsmopn  24842  zdis  24846  xrhmeo  24977  oprpiece1res1  24982  voliunlem3  25583  volsup  25587  volivth  25638  iblss2  25837  itgss  25843  coeidp  26292  dgrsub  26301  abelth  26470  reeff1olem  26475  sincosq1sgn  26529  sincosq3sgn  26531  sincosq4sgn  26532  sineq0  26555  logdivlt  26652  1cxp  26703  ecxp  26704  sinasin  26920  log2cnv  26975  efexple  27311  bposlem8  27321  lgsdir2lem2  27356  2sqb  27462  eqcuts2  27845  cutsun12  27849  eucliddivs  28435  pw2cut  28519  axpaschlem  29076  axlowdimlem9  29086  axlowdimlem12  29089  axlowdimlem16  29093  axlowdimlem17  29094  sizusglecusg  29599  clwlkclwwlkf  30145  imsmetlem  30828  nmoubi  30910  nmobndi  30913  nmounbi  30914  nmlno0lem  30931  nmlnoubi  30934  isblo3i  30939  blometi  30941  blocni  30943  blocn2  30946  ipasslem2  30970  siii  30991  ubthlem1  31008  ubthlem2  31009  ubthlem3  31010  htthlem  31055  hvsubid  31164  hv2times  31199  hi01  31234  hhssabloilem  31399  pjsumi  31848  mayete3i  31866  hoaddcomi  31910  hodsi  31913  hoaddassi  31914  hocadddiri  31917  hocsubdiri  31918  hoaddridi  31924  honegsubi  31934  honegneg  31944  ho2times  31957  eigrei  31972  eigorthi  31975  nmopnegi  32103  hoddii  32127  lnophsi  32139  lnopeqi  32146  nmoptrii  32232  opsqrlem1  32278  opsqrlem6  32283  pjsdii  32293  pjddii  32294  pjscji  32308  pjssposi  32310  pjssdif2i  32312  pjtoi  32317  mdsl2bi  32461  cvmdi  32462  mdslmd3i  32470  mdslmd4i  32471  mdexchi  32473  cvati  32504  cvexchlem  32506  mdsymi  32549  dmdbr5ati  32560  cdj1i  32571  cdj3lem1  32572  xrge0infss  32901  xrge0tsmsd  33203  elrspunidl  33560  2sqr3nconstr  34022  cos9thpinconstrlem2  34031  rrhre  34262  esumpinfval  34314  oms0  34538  eulerpartlems  34601  eulerpartlemgf  34620  probmeasb  34671  acycgr2v  35438  cvmliftlem5  35577  bcneg1  36024  wsuceq3  36103  fullfunfv  36235  finminlem  36616  nn0prpwlem  36620  regsfromunir1  36838  bj-ceqsalg0  37311  bj-ceqsalgALT  37313  bj-ceqsalgvALT  37315  bj-vtoclgfALT  37482  finxpreclem4  37826  sin2h  38047  cos2h  38048  tan2h  38049  poimirlem1  38058  poimirlem2  38059  poimirlem3  38060  poimirlem4  38061  poimirlem6  38063  poimirlem7  38064  poimirlem11  38068  poimirlem12  38069  poimirlem16  38073  poimirlem17  38074  poimirlem19  38076  poimirlem20  38077  poimirlem23  38080  poimirlem30  38087  poimirlem32  38089  poimir  38090  broucube  38091  mblfinlem1  38094  mblfinlem3  38096  mblfinlem4  38097  ismblfin  38098  volsupnfl  38102  iblmulc2nc  38122  ftc1anc  38138  dvasin  38141  heiborlem3  38250  heiborlem6  38253  heiborlem8  38255  cdleme32fva  40999  isnumbasgrplem1  43616  areaquad  43731  binomcxplemnotnn0  44870  permaxun  45525  fourierdlem101  46719  fourierdlem103  46721  fourierdlem104  46722  sqwvfourb  46741  fourierswlem  46742  fouriersw  46743  m1mod0mod1  47892  sgoldbeven3prm  48343  pgnbgreunbgrlem2lem1  48674  pgnbgreunbgrlem2lem2  48675  pgnbgreunbgrlem2lem3  48676  iooii  49477  aacllem  50360