Theorem mp3an12 1447

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 1085

This theorem is referenced by:  mp3an12i  1461  ceqsalg  3529  ceqsralv  3533  brelrn  5812  predeq3  6152  funpr  6410  tfi  7568  peano5  7605  wrecseq3  7952  wfr3  7975  fpm  8439  0fsupp  8855  ac6  9902  alephadd  9999  axpre-sup  10591  cnegex2  10822  addid2  10823  renegcli  10947  div0  11328  divclzi  11375  divcan1zi  11376  divcan2zi  11377  divreczi  11378  divcan3zi  11379  divcan4zi  11380  divasszi  11390  divmulzi  11391  divdirzi  11392  redivclzi  11406  ltm1  11482  mulgt1  11499  recgt1i  11537  ltmul1i  11558  ltdiv1i  11559  ltmuldivi  11560  ltmul2i  11561  lemul1i  11562  lemul2i  11563  ledivp1i  11565  ltdivp1i  11566  nnge1  11666  nngt0  11669  nnrecgt0  11681  nnunb  11894  recnz  12058  ge0gtmnf  12566  x2times  12693  xrub  12706  xrge0neqmnf  12841  1mod  13272  m1expcl2  13452  1exp  13459  expubnd  13542  iexpcyc  13570  expnbnd  13594  expnlbnd  13595  faclbnd4lem1  13654  imval2  14510  cjdivi  14550  resqrex  14610  sqrtneglem  14626  absdivzi  14767  climcndslem1  15204  climcndslem2  15205  fprodge1  15349  bpoly3  15412  sinhval  15507  coshval  15508  ef01bndlem  15537  sin01gt0  15543  cos01gt0  15544  evend2  15706  divalglem5  15748  vdwlem13  16329  prmlem1  16441  prmlem2  16453  ress0  16558  frmdplusg  18019  m1expaddsub  18626  islindf4  20982  resstopn  21794  lecldbas  21827  hmphindis  22405  cnbl0  23382  xrsmopn  23420  zdis  23424  xrhmeo  23550  oprpiece1res1  23555  voliunlem3  24153  volsup  24157  volivth  24208  iblss2  24406  itgss  24412  coeidp  24853  dgrsub  24862  abelth  25029  reeff1olem  25034  sincosq1sgn  25084  sincosq3sgn  25086  sincosq4sgn  25087  sineq0  25109  logdivlt  25204  1cxp  25255  ecxp  25256  sinasin  25467  log2cnv  25522  efexple  25857  bposlem8  25867  lgsdir2lem2  25902  2sqb  26008  axpaschlem  26726  axlowdimlem9  26736  axlowdimlem12  26739  axlowdimlem16  26743  axlowdimlem17  26744  sizusglecusg  27245  clwlkclwwlkf  27786  imsmetlem  28467  nmoubi  28549  nmobndi  28552  nmounbi  28553  nmlno0lem  28570  nmlnoubi  28573  isblo3i  28578  blometi  28580  blocni  28582  blocn2  28585  ipasslem2  28609  siii  28630  ubthlem1  28647  ubthlem2  28648  ubthlem3  28649  htthlem  28694  hvsubid  28803  hv2times  28838  hi01  28873  hhssabloilem  29038  pjsumi  29487  mayete3i  29505  hoaddcomi  29549  hodsi  29552  hoaddassi  29553  hocadddiri  29556  hocsubdiri  29557  hoaddid1i  29563  honegsubi  29573  honegneg  29583  ho2times  29596  eigrei  29611  eigorthi  29614  nmopnegi  29742  hoddii  29766  lnophsi  29778  lnopeqi  29785  nmoptrii  29871  opsqrlem1  29917  opsqrlem6  29922  pjsdii  29932  pjddii  29933  pjscji  29947  pjssposi  29949  pjssdif2i  29951  pjtoi  29956  mdsl2bi  30100  cvmdi  30101  mdslmd3i  30109  mdslmd4i  30110  mdexchi  30112  cvati  30143  cvexchlem  30145  mdsymi  30188  dmdbr5ati  30199  cdj1i  30210  cdj3lem1  30211  xrge0infss  30484  xrge0tsmsd  30692  rrhre  31262  esumpinfval  31332  oms0  31555  eulerpartlems  31618  eulerpartlemgf  31637  probmeasb  31688  acycgr2v  32397  cvmliftlem5  32536  bcneg1  32968  wsuceq3  33104  scutun12  33271  fullfunfv  33408  finminlem  33666  nn0prpwlem  33670  bj-ceqsalg0  34207  bj-ceqsalgALT  34209  bj-ceqsalgvALT  34211  bj-vtoclgfALT  34355  finxpreclem4  34678  sin2h  34897  cos2h  34898  tan2h  34899  poimirlem1  34908  poimirlem2  34909  poimirlem3  34910  poimirlem4  34911  poimirlem6  34913  poimirlem7  34914  poimirlem11  34918  poimirlem12  34919  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem23  34930  poimirlem30  34937  poimirlem32  34939  poimir  34940  broucube  34941  mblfinlem1  34944  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  volsupnfl  34952  itg2addnclem3  34960  iblmulc2nc  34972  ftc1anc  34990  dvasin  34993  heiborlem3  35106  heiborlem6  35109  heiborlem8  35111  cdleme32fva  37588  2xp3dxp2ge1d  39117  isnumbasgrplem1  39721  areaquad  39843  binomcxplemnotnn0  40708  fourierdlem101  42512  fourierdlem103  42514  fourierdlem104  42515  sqwvfourb  42534  fourierswlem  42535  fouriersw  42536  m1mod0mod1  43549  sgoldbeven3prm  43968  aacllem  44922