Theorem mp3an12 1480

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mp3an12i  1494  ceqsalg  3485  brelrn  5923  predeq3  6308  funpr  6596  fvpr1  7197  fvpr2  7198  tfi  7864  peano5  7905  wrecseq3  8335  fpm  8903  0fsupp  9382  ssttrcl  9716  ac6  10558  alephadd  10662  axpre-sup  11254  cnegex2  11492  addlid  11493  renegcli  11619  divclzi  12052  divcan1zi  12053  divcan2zi  12054  divreczi  12055  divcan3zi  12056  divcan4zi  12057  divasszi  12067  divmulzi  12068  divdirzi  12069  redivclzi  12083  ltm1  12159  recgt1i  12214  ltmul1i  12235  ltdiv1i  12236  ltmuldivi  12237  ltmul2i  12238  lemul1i  12239  lemul2i  12240  ledivp1i  12242  ltdivp1i  12243  nnge1  12366  nngt0  12369  nnrecgt0  12381  nnunb  12602  recnz  12774  eluzsubi  12997  ge0gtmnf  13302  x2times  13429  xrub  13442  xrge0neqmnf  13583  1mod  14043  m1expcl2  14228  1exp  14234  expubnd  14321  iexpcyc  14351  expnbnd  14376  expnlbnd  14377  faclbnd4lem1  14437  imval2  15318  cjdivi  15358  resqrex  15417  sqrtneglem  15433  absdivzi  15575  climcndslem1  16018  climcndslem2  16019  fprodge1  16162  bpoly3  16224  sinhval  16322  coshval  16323  ef01bndlem  16352  sin01gt0  16358  cos01gt0  16359  evend2  16527  divalglem5  16567  vdwlem13  17171  prmlem1  17285  prmlem2  17298  ress0  17421  frmdplusg  19050  m1expaddsub  19712  islindf4  22144  resstopn  23504  lecldbas  23537  hmphindis  24116  cnbl0  25092  xrsmopn  25132  zdis  25136  xrhmeo  25267  oprpiece1res1  25272  voliunlem3  25873  volsup  25877  volivth  25928  iblss2  26126  itgss  26132  coeidp  26582  dgrsub  26591  abelth  26768  reeff1olem  26773  sincosq1sgn  26827  sincosq3sgn  26829  sincosq4sgn  26830  sineq0  26852  logdivlt  26949  1cxp  27000  ecxp  27001  sinasin  27217  log2cnv  27272  efexple  27608  bposlem8  27618  lgsdir2lem2  27653  2sqb  27759  eqcuts2  28172  cutsun12  28176  eucliddivs  28762  pw2cut  28846  axpaschlem  29518  axlowdimlem9  29528  axlowdimlem12  29531  axlowdimlem16  29535  axlowdimlem17  29536  sizusglecusg  30044  clwlkclwwlkf  30599  imsmetlem  31292  nmoubi  31374  nmobndi  31377  nmounbi  31378  nmlno0lem  31395  nmlnoubi  31398  isblo3i  31403  blometi  31405  blocni  31407  blocn2  31410  ipasslem2  31434  siii  31455  ubthlem1  31472  ubthlem2  31473  ubthlem3  31474  htthlem  31519  hvsubid  31628  hv2times  31663  hi01  31698  hhssabloilem  31863  pjsumi  32312  mayete3i  32330  hoaddcomi  32374  hodsi  32377  hoaddassi  32378  hocadddiri  32381  hocsubdiri  32382  hoaddridi  32388  honegsubi  32398  honegneg  32408  ho2times  32421  eigrei  32436  eigorthi  32439  nmopnegi  32567  hoddii  32591  lnophsi  32603  lnopeqi  32610  nmoptrii  32696  opsqrlem1  32742  opsqrlem6  32747  pjsdii  32757  pjddii  32758  pjscji  32772  pjssposi  32774  pjssdif2i  32776  pjtoi  32781  mdsl2bi  32925  cvmdi  32926  mdslmd3i  32934  mdslmd4i  32935  mdexchi  32937  cvati  32968  cvexchlem  32970  mdsymi  33013  dmdbr5ati  33024  cdj1i  33035  cdj3lem1  33036  xrge0infss  33394  xrge0tsmsd  33676  elrspunidl  34020  2sqr3nconstr  34455  cos9thpinconstrlem2  34464  rrhre  34695  esumpinfval  34747  oms0  34971  eulerpartlems  35034  eulerpartlemgf  35053  probmeasb  35104  dfscott2  35784  dfscott3  35785  acycgr2v  35957  cvmliftlem5  36096  bcneg1  36543  wsuceq3  36621  fullfunfv  36753  finminlem  37148  nn0prpwlem  37152  regsfromunir1  37370  bj-ceqsalg0  37842  bj-ceqsalgALT  37844  bj-ceqsalgvALT  37846  bj-vtoclgfALT  38016  finxpreclem4  38360  sin2h  38576  cos2h  38577  tan2h  38578  poimirlem1  38582  poimirlem2  38583  poimirlem3  38584  poimirlem4  38585  poimirlem6  38587  poimirlem7  38588  poimirlem11  38592  poimirlem12  38593  poimirlem16  38597  poimirlem17  38598  poimirlem19  38600  poimirlem20  38601  poimirlem23  38604  poimirlem30  38611  poimirlem32  38613  poimir  38614  broucube  38615  mblfinlem1  38618  mblfinlem3  38620  mblfinlem4  38621  ismblfin  38622  volsupnfl  38626  iblmulc2nc  38646  ftc1anc  38662  dvasin  38665  heiborlem3  38790  heiborlem6  38793  heiborlem8  38795  cdleme32fva  41537  frlmnzcoordinf  43697  isnumbasgrplem1  44146  areaquad  44261  binomcxplemnotnn0  45383  permaxun  46044  fourierdlem101  47260  fourierdlem103  47262  fourierdlem104  47263  sqwvfourb  47282  fourierswlem  47283  fouriersw  47284  m1mod0mod1  48473  sgoldbeven3prm  48924  pgnbgreunbgrlem2lem1  49255  pgnbgreunbgrlem2lem2  49256  pgnbgreunbgrlem2lem3  49257  iooii  50069  aacllem  50982