Theorem mp3an12 1452

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 1449	. 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  1466  ceqsalg  3516  brelrn  5952  predeq3  6324  funpr  6621  fvpr1  7213  fvpr2  7214  tfi  7875  peano5  7916  wrecseq3  8346  wfr3OLD  8379  fpm  8916  0fsupp  9431  ssttrcl  9756  ac6  10521  alephadd  10618  axpre-sup  11210  cnegex2  11444  addlid  11445  renegcli  11571  div0OLD  11957  divclzi  12003  divcan1zi  12004  divcan2zi  12005  divreczi  12006  divcan3zi  12007  divcan4zi  12008  divasszi  12018  divmulzi  12019  divdirzi  12020  redivclzi  12034  ltm1  12110  mulgt1OLD  12127  recgt1i  12166  ltmul1i  12187  ltdiv1i  12188  ltmuldivi  12189  ltmul2i  12190  lemul1i  12191  lemul2i  12192  ledivp1i  12194  ltdivp1i  12195  nnge1  12295  nngt0  12298  nnrecgt0  12310  nnunb  12524  recnz  12695  eluzsubi  12912  ge0gtmnf  13215  x2times  13342  xrub  13355  xrge0neqmnf  13493  1mod  13944  m1expcl2  14127  1exp  14133  expubnd  14218  iexpcyc  14247  expnbnd  14272  expnlbnd  14273  faclbnd4lem1  14333  imval2  15191  cjdivi  15231  resqrex  15290  sqrtneglem  15306  absdivzi  15447  climcndslem1  15886  climcndslem2  15887  fprodge1  16032  bpoly3  16095  sinhval  16191  coshval  16192  ef01bndlem  16221  sin01gt0  16227  cos01gt0  16228  evend2  16395  divalglem5  16435  vdwlem13  17032  prmlem1  17146  prmlem2  17158  ress0  17290  frmdplusg  18868  m1expaddsub  19517  islindf4  21859  resstopn  23195  lecldbas  23228  hmphindis  23806  cnbl0  24795  xrsmopn  24835  zdis  24839  xrhmeo  24978  oprpiece1res1  24983  voliunlem3  25588  volsup  25592  volivth  25643  iblss2  25842  itgss  25848  coeidp  26304  dgrsub  26313  abelth  26486  reeff1olem  26491  sincosq1sgn  26541  sincosq3sgn  26543  sincosq4sgn  26544  sineq0  26567  logdivlt  26664  1cxp  26715  ecxp  26716  sinasin  26933  log2cnv  26988  efexple  27326  bposlem8  27336  lgsdir2lem2  27371  2sqb  27477  eqscut2  27852  scutun12  27856  cutpw2  28418  pw2bday  28419  pw2cut  28421  zs12bday  28425  axpaschlem  28956  axlowdimlem9  28966  axlowdimlem12  28969  axlowdimlem16  28973  axlowdimlem17  28974  sizusglecusg  29482  clwlkclwwlkf  30028  imsmetlem  30710  nmoubi  30792  nmobndi  30795  nmounbi  30796  nmlno0lem  30813  nmlnoubi  30816  isblo3i  30821  blometi  30823  blocni  30825  blocn2  30828  ipasslem2  30852  siii  30873  ubthlem1  30890  ubthlem2  30891  ubthlem3  30892  htthlem  30937  hvsubid  31046  hv2times  31081  hi01  31116  hhssabloilem  31281  pjsumi  31730  mayete3i  31748  hoaddcomi  31792  hodsi  31795  hoaddassi  31796  hocadddiri  31799  hocsubdiri  31800  hoaddridi  31806  honegsubi  31816  honegneg  31826  ho2times  31839  eigrei  31854  eigorthi  31857  nmopnegi  31985  hoddii  32009  lnophsi  32021  lnopeqi  32028  nmoptrii  32114  opsqrlem1  32160  opsqrlem6  32165  pjsdii  32175  pjddii  32176  pjscji  32190  pjssposi  32192  pjssdif2i  32194  pjtoi  32199  mdsl2bi  32343  cvmdi  32344  mdslmd3i  32352  mdslmd4i  32353  mdexchi  32355  cvati  32386  cvexchlem  32388  mdsymi  32431  dmdbr5ati  32442  cdj1i  32453  cdj3lem1  32454  xrge0infss  32765  xrge0tsmsd  33066  elrspunidl  33457  rrhre  34023  esumpinfval  34075  oms0  34300  eulerpartlems  34363  eulerpartlemgf  34382  probmeasb  34433  acycgr2v  35156  cvmliftlem5  35295  bcneg1  35737  wsuceq3  35819  fullfunfv  35949  finminlem  36320  nn0prpwlem  36324  bj-ceqsalg0  36890  bj-ceqsalgALT  36892  bj-ceqsalgvALT  36894  bj-vtoclgfALT  37061  finxpreclem4  37396  sin2h  37618  cos2h  37619  tan2h  37620  poimirlem1  37629  poimirlem2  37630  poimirlem3  37631  poimirlem4  37632  poimirlem6  37634  poimirlem7  37635  poimirlem11  37639  poimirlem12  37640  poimirlem16  37644  poimirlem17  37645  poimirlem19  37647  poimirlem20  37648  poimirlem23  37651  poimirlem30  37658  poimirlem32  37660  poimir  37661  broucube  37662  mblfinlem1  37665  mblfinlem3  37667  mblfinlem4  37668  ismblfin  37669  volsupnfl  37673  iblmulc2nc  37693  ftc1anc  37709  dvasin  37712  heiborlem3  37821  heiborlem6  37824  heiborlem8  37826  cdleme32fva  40440  2xp3dxp2ge1d  42243  isnumbasgrplem1  43118  areaquad  43233  binomcxplemnotnn0  44380  fourierdlem101  46227  fourierdlem103  46229  fourierdlem104  46230  sqwvfourb  46249  fourierswlem  46250  fouriersw  46251  m1mod0mod1  47361  sgoldbeven3prm  47775  iooii  48822  aacllem  49375