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  3480  brelrn  5895  predeq3  6266  funpr  6556  fvpr1  7148  fvpr2  7149  tfi  7809  peano5  7849  wrecseq3  8273  fpm  8825  0fsupp  9317  ssttrcl  9646  ac6  10411  alephadd  10508  axpre-sup  11100  cnegex2  11334  addlid  11335  renegcli  11461  div0OLD  11849  divclzi  11895  divcan1zi  11896  divcan2zi  11897  divreczi  11898  divcan3zi  11899  divcan4zi  11900  divasszi  11910  divmulzi  11911  divdirzi  11912  redivclzi  11926  ltm1  12002  mulgt1OLD  12019  recgt1i  12058  ltmul1i  12079  ltdiv1i  12080  ltmuldivi  12081  ltmul2i  12082  lemul1i  12083  lemul2i  12084  ledivp1i  12086  ltdivp1i  12087  nnge1  12192  nngt0  12195  nnrecgt0  12207  nnunb  12416  recnz  12587  eluzsubi  12804  ge0gtmnf  13110  x2times  13237  xrub  13250  xrge0neqmnf  13391  1mod  13843  m1expcl2  14028  1exp  14034  expubnd  14121  iexpcyc  14150  expnbnd  14175  expnlbnd  14176  faclbnd4lem1  14236  imval2  15094  cjdivi  15134  resqrex  15193  sqrtneglem  15209  absdivzi  15351  climcndslem1  15792  climcndslem2  15793  fprodge1  15938  bpoly3  16001  sinhval  16099  coshval  16100  ef01bndlem  16129  sin01gt0  16135  cos01gt0  16136  evend2  16304  divalglem5  16344  vdwlem13  16941  prmlem1  17055  prmlem2  17067  ress0  17190  frmdplusg  18764  m1expaddsub  19413  islindf4  21781  resstopn  23107  lecldbas  23140  hmphindis  23718  cnbl0  24695  xrsmopn  24735  zdis  24739  xrhmeo  24878  oprpiece1res1  24883  voliunlem3  25487  volsup  25491  volivth  25542  iblss2  25741  itgss  25747  coeidp  26203  dgrsub  26212  abelth  26385  reeff1olem  26390  sincosq1sgn  26441  sincosq3sgn  26443  sincosq4sgn  26444  sineq0  26467  logdivlt  26564  1cxp  26615  ecxp  26616  sinasin  26833  log2cnv  26888  efexple  27226  bposlem8  27236  lgsdir2lem2  27271  2sqb  27377  eqscut2  27753  scutun12  27757  eucliddivs  28306  pw2cut  28384  zs12bday  28397  axpaschlem  28921  axlowdimlem9  28931  axlowdimlem12  28934  axlowdimlem16  28938  axlowdimlem17  28939  sizusglecusg  29445  clwlkclwwlkf  29988  imsmetlem  30670  nmoubi  30752  nmobndi  30755  nmounbi  30756  nmlno0lem  30773  nmlnoubi  30776  isblo3i  30781  blometi  30783  blocni  30785  blocn2  30788  ipasslem2  30812  siii  30833  ubthlem1  30850  ubthlem2  30851  ubthlem3  30852  htthlem  30897  hvsubid  31006  hv2times  31041  hi01  31076  hhssabloilem  31241  pjsumi  31690  mayete3i  31708  hoaddcomi  31752  hodsi  31755  hoaddassi  31756  hocadddiri  31759  hocsubdiri  31760  hoaddridi  31766  honegsubi  31776  honegneg  31786  ho2times  31799  eigrei  31814  eigorthi  31817  nmopnegi  31945  hoddii  31969  lnophsi  31981  lnopeqi  31988  nmoptrii  32074  opsqrlem1  32120  opsqrlem6  32125  pjsdii  32135  pjddii  32136  pjscji  32150  pjssposi  32152  pjssdif2i  32154  pjtoi  32159  mdsl2bi  32303  cvmdi  32304  mdslmd3i  32312  mdslmd4i  32313  mdexchi  32315  cvati  32346  cvexchlem  32348  mdsymi  32391  dmdbr5ati  32402  cdj1i  32413  cdj3lem1  32414  xrge0infss  32734  xrge0tsmsd  33046  elrspunidl  33393  2sqr3nconstr  33765  cos9thpinconstrlem2  33774  rrhre  34005  esumpinfval  34057  oms0  34282  eulerpartlems  34345  eulerpartlemgf  34364  probmeasb  34415  acycgr2v  35131  cvmliftlem5  35270  bcneg1  35717  wsuceq3  35799  fullfunfv  35929  finminlem  36300  nn0prpwlem  36304  bj-ceqsalg0  36870  bj-ceqsalgALT  36872  bj-ceqsalgvALT  36874  bj-vtoclgfALT  37041  finxpreclem4  37376  sin2h  37598  cos2h  37599  tan2h  37600  poimirlem1  37609  poimirlem2  37610  poimirlem3  37611  poimirlem4  37612  poimirlem6  37614  poimirlem7  37615  poimirlem11  37619  poimirlem12  37620  poimirlem16  37624  poimirlem17  37625  poimirlem19  37627  poimirlem20  37628  poimirlem23  37631  poimirlem30  37638  poimirlem32  37640  poimir  37641  broucube  37642  mblfinlem1  37645  mblfinlem3  37647  mblfinlem4  37648  ismblfin  37649  volsupnfl  37653  iblmulc2nc  37673  ftc1anc  37689  dvasin  37692  heiborlem3  37801  heiborlem6  37804  heiborlem8  37806  cdleme32fva  40425  isnumbasgrplem1  43084  areaquad  43199  binomcxplemnotnn0  44339  permaxun  44995  fourierdlem101  46199  fourierdlem103  46201  fourierdlem104  46202  sqwvfourb  46221  fourierswlem  46222  fouriersw  46223  m1mod0mod1  47349  sgoldbeven3prm  47778  pgnbgreunbgrlem2lem1  48098  pgnbgreunbgrlem2lem2  48099  pgnbgreunbgrlem2lem3  48100  iooii  48900  aacllem  49784