Theorem mp3an12 1524

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

Syntax hints:   → wi 4   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  mp3an12i  1538  ceqsalg  3432  ceqsralv  3436  brelrn  5602  predeq3  5937  funpr  6190  tfi  7331  peano5  7367  wrecseq3  7694  wfr3  7718  fpm  8173  0fsupp  8585  ac6  9637  alephadd  9734  axpre-sup  10326  cnegex2  10558  addid2  10559  renegcli  10684  div0  11063  divclzi  11110  divcan1zi  11111  divcan2zi  11112  divreczi  11113  divcan3zi  11114  divcan4zi  11115  divasszi  11125  divmulzi  11126  divdirzi  11127  redivclzi  11141  ltm1  11217  mulgt1  11236  recgt1i  11274  ltmul1i  11296  ltdiv1i  11297  ltmuldivi  11298  ltmul2i  11299  lemul1i  11300  lemul2i  11301  ledivp1i  11303  ltdivp1i  11304  nnge1  11404  nngt0  11407  nnrecgt0  11418  nnunb  11638  recnz  11804  ge0gtmnf  12315  x2times  12441  xrub  12454  xrge0neqmnf  12589  1mod  13021  m1expcl2  13200  1exp  13207  expubnd  13239  iexpcyc  13288  expnbnd  13312  expnlbnd  13313  faclbnd4lem1  13398  imval2  14298  cjdivi  14338  resqrex  14398  sqrtneglem  14414  absdivzi  14554  climcndslem1  14985  climcndslem2  14986  fprodge1  15128  bpoly3  15191  sinhval  15286  coshval  15287  ef01bndlem  15316  sin01gt0  15322  cos01gt0  15323  evend2  15485  divalglem5  15527  vdwlem13  16101  prmlem1  16213  prmlem2  16225  ress0  16330  frmdplusg  17778  symggen  18273  m1expaddsub  18302  psgnuni  18303  islindf4  20581  resstopn  21398  lecldbas  21431  hmphindis  22009  cnbl0  22985  xrsmopn  23023  zdis  23027  reperflem  23029  xrge0tsms  23045  xrhmeo  23153  oprpiece1res1  23158  cphsqrtcl  23391  ovolicopnf  23728  voliunlem3  23756  volsup  23760  volivth  23811  itg2seq  23946  itg2monolem2  23955  itgz  23984  ibl0  23990  iblss  24008  iblss2  24009  itgss  24015  itgeqa  24017  iblconst  24021  iblabsr  24033  iblmulc2  24034  itgsplit  24039  coeidp  24456  dgrsub  24465  aaliou3lem2  24535  abelth  24632  reeff1olem  24637  pilem3OLD  24645  sincosq1sgn  24688  sincosq3sgn  24690  sincosq4sgn  24691  sineq0  24711  resinf1o  24720  efif1olem4  24729  logdivlti  24803  logdivlt  24804  efopn  24841  1cxp  24855  ecxp  24856  cxpsqrt  24886  isosctrlem1  24996  sinasin  25067  asinsin  25070  log2cnv  25123  basellem2  25260  basellem3  25261  isnsqf  25313  ppidif  25341  ppiublem1  25379  efexple  25458  bposlem6  25466  bposlem8  25468  lgsdir2lem2  25503  2sqb  25609  ostth3  25779  axpaschlem  26289  axlowdimlem3  26293  axlowdimlem7  26297  axlowdimlem9  26299  axlowdimlem12  26302  axlowdimlem16  26306  axlowdimlem17  26307  axlowdim  26310  sizusglecusg  26811  clwlkclwwlkfOLD  27392  clwlkclwwlkf  27396  imsmetlem  28117  nmoubi  28199  nmobndi  28202  nmounbi  28203  nmlno0lem  28220  nmlnoubi  28223  isblo3i  28228  blometi  28230  blocni  28232  blocn2  28235  ipasslem2  28259  siii  28280  ubthlem1  28298  ubthlem2  28299  ubthlem3  28300  htthlem  28346  hvsubid  28455  hv2times  28490  hi01  28525  hhssabloilem  28690  pjsumi  29141  mayete3i  29159  hoaddcomi  29203  hodsi  29206  hoaddassi  29207  hocadddiri  29210  hocsubdiri  29211  hoaddid1i  29217  honegsubi  29227  honegneg  29237  ho2times  29250  eigrei  29265  eigorthi  29268  nmopnegi  29396  hoddii  29420  lnophsi  29432  lnopeqi  29439  nmoptrii  29525  opsqrlem1  29571  opsqrlem6  29576  pjsdii  29586  pjddii  29587  pjscji  29601  pjssposi  29603  pjssdif2i  29605  pjtoi  29610  mdsl2bi  29754  cvmdi  29755  mdslmd3i  29763  mdslmd4i  29764  mdexchi  29766  cvati  29797  cvexchlem  29799  mdsymi  29842  dmdbr5ati  29853  cdj1i  29864  cdj3lem1  29865  xrge0infss  30090  xrge0tsmsd  30347  rrhre  30663  esumpinfval  30733  oms0  30957  eulerpartlems  31020  eulerpartlemgf  31039  probmeasb  31091  cvmliftlem5  31870  bcneg1  32216  wsuceq3  32351  scutun12  32506  fullfunfv  32643  finminlem  32901  nn0prpwlem  32905  bj-ceqsalg0  33447  bj-ceqsalgALT  33449  bj-ceqsalgvALT  33451  bj-vtoclgfALT  33593  finxpreclem4  33826  sin2h  34024  cos2h  34025  tan2h  34026  poimirlem1  34036  poimirlem2  34037  poimirlem3  34038  poimirlem4  34039  poimirlem6  34041  poimirlem7  34042  poimirlem11  34046  poimirlem12  34047  poimirlem16  34051  poimirlem17  34052  poimirlem19  34054  poimirlem20  34055  poimirlem23  34058  poimirlem30  34065  poimirlem32  34067  poimir  34068  broucube  34069  mblfinlem1  34072  mblfinlem3  34074  mblfinlem4  34075  ismblfin  34076  volsupnfl  34080  itg2addnclem3  34088  iblmulc2nc  34100  ftc1anc  34118  dvasin  34121  heiborlem3  34236  heiborlem6  34239  heiborlem8  34241  cdleme32fva  36591  isnumbasgrplem1  38630  areaquad  38760  binomcxplemnotnn0  39511  fourierdlem101  41351  fourierdlem103  41353  fourierdlem104  41354  sqwvfourb  41373  fourierswlem  41374  fouriersw  41375  m1mod0mod1  42371  sgoldbeven3prm  42696  aacllem  43653