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  5896  predeq3  6267  funpr  6557  fvpr1  7149  fvpr2  7150  tfi  7810  peano5  7850  wrecseq3  8274  fpm  8826  0fsupp  9318  ssttrcl  9647  ac6  10412  alephadd  10509  axpre-sup  11101  cnegex2  11335  addlid  11336  renegcli  11462  div0OLD  11850  divclzi  11896  divcan1zi  11897  divcan2zi  11898  divreczi  11899  divcan3zi  11900  divcan4zi  11901  divasszi  11911  divmulzi  11912  divdirzi  11913  redivclzi  11927  ltm1  12003  mulgt1OLD  12020  recgt1i  12059  ltmul1i  12080  ltdiv1i  12081  ltmuldivi  12082  ltmul2i  12083  lemul1i  12084  lemul2i  12085  ledivp1i  12087  ltdivp1i  12088  nnge1  12193  nngt0  12196  nnrecgt0  12208  nnunb  12417  recnz  12588  eluzsubi  12805  ge0gtmnf  13111  x2times  13238  xrub  13251  xrge0neqmnf  13392  1mod  13844  m1expcl2  14029  1exp  14035  expubnd  14122  iexpcyc  14151  expnbnd  14176  expnlbnd  14177  faclbnd4lem1  14237  imval2  15095  cjdivi  15135  resqrex  15194  sqrtneglem  15210  absdivzi  15352  climcndslem1  15793  climcndslem2  15794  fprodge1  15939  bpoly3  16002  sinhval  16100  coshval  16101  ef01bndlem  16130  sin01gt0  16136  cos01gt0  16137  evend2  16305  divalglem5  16345  vdwlem13  16942  prmlem1  17056  prmlem2  17068  ress0  17191  frmdplusg  18765  m1expaddsub  19414  islindf4  21782  resstopn  23108  lecldbas  23141  hmphindis  23719  cnbl0  24696  xrsmopn  24736  zdis  24740  xrhmeo  24879  oprpiece1res1  24884  voliunlem3  25488  volsup  25492  volivth  25543  iblss2  25742  itgss  25748  coeidp  26204  dgrsub  26213  abelth  26386  reeff1olem  26391  sincosq1sgn  26442  sincosq3sgn  26444  sincosq4sgn  26445  sineq0  26468  logdivlt  26565  1cxp  26616  ecxp  26617  sinasin  26834  log2cnv  26889  efexple  27227  bposlem8  27237  lgsdir2lem2  27272  2sqb  27378  eqscut2  27754  scutun12  27758  eucliddivs  28307  pw2cut  28385  zs12bday  28398  axpaschlem  28922  axlowdimlem9  28932  axlowdimlem12  28935  axlowdimlem16  28939  axlowdimlem17  28940  sizusglecusg  29446  clwlkclwwlkf  29989  imsmetlem  30671  nmoubi  30753  nmobndi  30756  nmounbi  30757  nmlno0lem  30774  nmlnoubi  30777  isblo3i  30782  blometi  30784  blocni  30786  blocn2  30789  ipasslem2  30813  siii  30834  ubthlem1  30851  ubthlem2  30852  ubthlem3  30853  htthlem  30898  hvsubid  31007  hv2times  31042  hi01  31077  hhssabloilem  31242  pjsumi  31691  mayete3i  31709  hoaddcomi  31753  hodsi  31756  hoaddassi  31757  hocadddiri  31760  hocsubdiri  31761  hoaddridi  31767  honegsubi  31777  honegneg  31787  ho2times  31800  eigrei  31815  eigorthi  31818  nmopnegi  31946  hoddii  31970  lnophsi  31982  lnopeqi  31989  nmoptrii  32075  opsqrlem1  32121  opsqrlem6  32126  pjsdii  32136  pjddii  32137  pjscji  32151  pjssposi  32153  pjssdif2i  32155  pjtoi  32160  mdsl2bi  32304  cvmdi  32305  mdslmd3i  32313  mdslmd4i  32314  mdexchi  32316  cvati  32347  cvexchlem  32349  mdsymi  32392  dmdbr5ati  32403  cdj1i  32414  cdj3lem1  32415  xrge0infss  32735  xrge0tsmsd  33047  elrspunidl  33394  2sqr3nconstr  33766  cos9thpinconstrlem2  33775  rrhre  34006  esumpinfval  34058  oms0  34283  eulerpartlems  34346  eulerpartlemgf  34365  probmeasb  34416  acycgr2v  35132  cvmliftlem5  35271  bcneg1  35718  wsuceq3  35800  fullfunfv  35930  finminlem  36301  nn0prpwlem  36305  bj-ceqsalg0  36871  bj-ceqsalgALT  36873  bj-ceqsalgvALT  36875  bj-vtoclgfALT  37042  finxpreclem4  37377  sin2h  37599  cos2h  37600  tan2h  37601  poimirlem1  37610  poimirlem2  37611  poimirlem3  37612  poimirlem4  37613  poimirlem6  37615  poimirlem7  37616  poimirlem11  37620  poimirlem12  37621  poimirlem16  37625  poimirlem17  37626  poimirlem19  37628  poimirlem20  37629  poimirlem23  37632  poimirlem30  37639  poimirlem32  37641  poimir  37642  broucube  37643  mblfinlem1  37646  mblfinlem3  37648  mblfinlem4  37649  ismblfin  37650  volsupnfl  37654  iblmulc2nc  37674  ftc1anc  37690  dvasin  37693  heiborlem3  37802  heiborlem6  37805  heiborlem8  37807  cdleme32fva  40426  isnumbasgrplem1  43085  areaquad  43200  binomcxplemnotnn0  44340  permaxun  44996  fourierdlem101  46200  fourierdlem103  46202  fourierdlem104  46203  sqwvfourb  46222  fourierswlem  46223  fouriersw  46224  m1mod0mod1  47350  sgoldbeven3prm  47779  pgnbgreunbgrlem2lem1  48099  pgnbgreunbgrlem2lem2  48100  pgnbgreunbgrlem2lem3  48101  iooii  48901  aacllem  49785