Theorem mp3an12 1447

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  mp3an12i  1461  ceqsalg  3531  ceqsralv  3535  brelrn  5814  predeq3  6154  funpr  6412  tfi  7570  peano5  7607  wrecseq3  7954  wfr3  7977  fpm  8441  0fsupp  8857  ac6  9904  alephadd  10001  axpre-sup  10593  cnegex2  10824  addid2  10825  renegcli  10949  div0  11330  divclzi  11377  divcan1zi  11378  divcan2zi  11379  divreczi  11380  divcan3zi  11381  divcan4zi  11382  divasszi  11392  divmulzi  11393  divdirzi  11394  redivclzi  11408  ltm1  11484  mulgt1  11501  recgt1i  11539  ltmul1i  11560  ltdiv1i  11561  ltmuldivi  11562  ltmul2i  11563  lemul1i  11564  lemul2i  11565  ledivp1i  11567  ltdivp1i  11568  nnge1  11668  nngt0  11671  nnrecgt0  11683  nnunb  11896  recnz  12060  ge0gtmnf  12568  x2times  12695  xrub  12708  xrge0neqmnf  12843  1mod  13274  m1expcl2  13454  1exp  13461  expubnd  13544  iexpcyc  13572  expnbnd  13596  expnlbnd  13597  faclbnd4lem1  13656  imval2  14512  cjdivi  14552  resqrex  14612  sqrtneglem  14628  absdivzi  14769  climcndslem1  15206  climcndslem2  15207  fprodge1  15351  bpoly3  15414  sinhval  15509  coshval  15510  ef01bndlem  15539  sin01gt0  15545  cos01gt0  15546  evend2  15708  divalglem5  15750  vdwlem13  16331  prmlem1  16443  prmlem2  16455  ress0  16560  frmdplusg  18021  m1expaddsub  18628  islindf4  20984  resstopn  21796  lecldbas  21829  hmphindis  22407  cnbl0  23384  xrsmopn  23422  zdis  23426  xrhmeo  23552  oprpiece1res1  23557  voliunlem3  24155  volsup  24159  volivth  24210  iblss2  24408  itgss  24414  coeidp  24855  dgrsub  24864  abelth  25031  reeff1olem  25036  sincosq1sgn  25086  sincosq3sgn  25088  sincosq4sgn  25089  sineq0  25111  logdivlt  25206  1cxp  25257  ecxp  25258  sinasin  25469  log2cnv  25524  efexple  25859  bposlem8  25869  lgsdir2lem2  25904  2sqb  26010  axpaschlem  26728  axlowdimlem9  26738  axlowdimlem12  26741  axlowdimlem16  26745  axlowdimlem17  26746  sizusglecusg  27247  clwlkclwwlkf  27788  imsmetlem  28469  nmoubi  28551  nmobndi  28554  nmounbi  28555  nmlno0lem  28572  nmlnoubi  28575  isblo3i  28580  blometi  28582  blocni  28584  blocn2  28587  ipasslem2  28611  siii  28632  ubthlem1  28649  ubthlem2  28650  ubthlem3  28651  htthlem  28696  hvsubid  28805  hv2times  28840  hi01  28875  hhssabloilem  29040  pjsumi  29489  mayete3i  29507  hoaddcomi  29551  hodsi  29554  hoaddassi  29555  hocadddiri  29558  hocsubdiri  29559  hoaddid1i  29565  honegsubi  29575  honegneg  29585  ho2times  29598  eigrei  29613  eigorthi  29616  nmopnegi  29744  hoddii  29768  lnophsi  29780  lnopeqi  29787  nmoptrii  29873  opsqrlem1  29919  opsqrlem6  29924  pjsdii  29934  pjddii  29935  pjscji  29949  pjssposi  29951  pjssdif2i  29953  pjtoi  29958  mdsl2bi  30102  cvmdi  30103  mdslmd3i  30111  mdslmd4i  30112  mdexchi  30114  cvati  30145  cvexchlem  30147  mdsymi  30190  dmdbr5ati  30201  cdj1i  30212  cdj3lem1  30213  xrge0infss  30486  xrge0tsmsd  30694  rrhre  31264  esumpinfval  31334  oms0  31557  eulerpartlems  31620  eulerpartlemgf  31639  probmeasb  31690  acycgr2v  32399  cvmliftlem5  32538  bcneg1  32970  wsuceq3  33106  scutun12  33273  fullfunfv  33410  finminlem  33668  nn0prpwlem  33672  bj-ceqsalg0  34206  bj-ceqsalgALT  34208  bj-ceqsalgvALT  34210  bj-vtoclgfALT  34354  finxpreclem4  34677  sin2h  34884  cos2h  34885  tan2h  34886  poimirlem1  34895  poimirlem2  34896  poimirlem3  34897  poimirlem4  34898  poimirlem6  34900  poimirlem7  34901  poimirlem11  34905  poimirlem12  34906  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem23  34917  poimirlem30  34924  poimirlem32  34926  poimir  34927  broucube  34928  mblfinlem1  34931  mblfinlem3  34933  mblfinlem4  34934  ismblfin  34935  volsupnfl  34939  itg2addnclem3  34947  iblmulc2nc  34959  ftc1anc  34977  dvasin  34980  heiborlem3  35093  heiborlem6  35096  heiborlem8  35098  cdleme32fva  37575  2xp3dxp2ge1d  39104  isnumbasgrplem1  39708  areaquad  39830  binomcxplemnotnn0  40695  fourierdlem101  42499  fourierdlem103  42501  fourierdlem104  42502  sqwvfourb  42521  fourierswlem  42522  fouriersw  42523  m1mod0mod1  43536  sgoldbeven3prm  43955  aacllem  44909