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  5920  predeq3  6297  funpr  6584  fvpr1  7185  fvpr2  7186  tfi  7847  peano5  7888  wrecseq3  8313  fpm  8881  0fsupp  9360  ssttrcl  9694  ac6  10529  alephadd  10633  axpre-sup  11225  cnegex2  11463  addlid  11464  renegcli  11590  divclzi  12021  divcan1zi  12022  divcan2zi  12023  divreczi  12024  divcan3zi  12025  divcan4zi  12026  divasszi  12036  divmulzi  12037  divdirzi  12038  redivclzi  12052  ltm1  12128  recgt1i  12183  ltmul1i  12204  ltdiv1i  12205  ltmuldivi  12206  ltmul2i  12207  lemul1i  12208  lemul2i  12209  ledivp1i  12211  ltdivp1i  12212  nnge1  12335  nngt0  12338  nnrecgt0  12350  nnunb  12571  recnz  12743  eluzsubi  12966  ge0gtmnf  13271  x2times  13398  xrub  13411  xrge0neqmnf  13552  1mod  14011  m1expcl2  14196  1exp  14202  expubnd  14289  iexpcyc  14318  expnbnd  14343  expnlbnd  14344  faclbnd4lem1  14404  imval2  15285  cjdivi  15325  resqrex  15384  sqrtneglem  15400  absdivzi  15542  climcndslem1  15985  climcndslem2  15986  fprodge1  16129  bpoly3  16191  sinhval  16289  coshval  16290  ef01bndlem  16319  sin01gt0  16325  cos01gt0  16326  evend2  16494  divalglem5  16534  vdwlem13  17132  prmlem1  17246  prmlem2  17259  ress0  17382  frmdplusg  19011  m1expaddsub  19673  islindf4  22105  resstopn  23465  lecldbas  23498  hmphindis  24077  cnbl0  25053  xrsmopn  25093  zdis  25097  xrhmeo  25228  oprpiece1res1  25233  voliunlem3  25834  volsup  25838  volivth  25889  iblss2  26087  itgss  26093  coeidp  26543  dgrsub  26552  abelth  26731  reeff1olem  26736  sincosq1sgn  26790  sincosq3sgn  26792  sincosq4sgn  26793  sineq0  26815  logdivlt  26912  1cxp  26963  ecxp  26964  sinasin  27180  log2cnv  27235  efexple  27571  bposlem8  27581  lgsdir2lem2  27616  2sqb  27722  eqcuts2  28105  cutsun12  28109  eucliddivs  28695  pw2cut  28779  axpaschlem  29451  axlowdimlem9  29461  axlowdimlem12  29464  axlowdimlem16  29468  axlowdimlem17  29469  sizusglecusg  29977  clwlkclwwlkf  30532  imsmetlem  31225  nmoubi  31307  nmobndi  31310  nmounbi  31311  nmlno0lem  31328  nmlnoubi  31331  isblo3i  31336  blometi  31338  blocni  31340  blocn2  31343  ipasslem2  31367  siii  31388  ubthlem1  31405  ubthlem2  31406  ubthlem3  31407  htthlem  31452  hvsubid  31561  hv2times  31596  hi01  31631  hhssabloilem  31796  pjsumi  32245  mayete3i  32263  hoaddcomi  32307  hodsi  32310  hoaddassi  32311  hocadddiri  32314  hocsubdiri  32315  hoaddridi  32321  honegsubi  32331  honegneg  32341  ho2times  32354  eigrei  32369  eigorthi  32372  nmopnegi  32500  hoddii  32524  lnophsi  32536  lnopeqi  32543  nmoptrii  32629  opsqrlem1  32675  opsqrlem6  32680  pjsdii  32690  pjddii  32691  pjscji  32705  pjssposi  32707  pjssdif2i  32709  pjtoi  32714  mdsl2bi  32858  cvmdi  32859  mdslmd3i  32867  mdslmd4i  32868  mdexchi  32870  cvati  32901  cvexchlem  32903  mdsymi  32946  dmdbr5ati  32957  cdj1i  32968  cdj3lem1  32969  xrge0infss  33285  xrge0tsmsd  33567  elrspunidl  33911  2sqr3nconstr  34346  cos9thpinconstrlem2  34355  rrhre  34586  esumpinfval  34638  oms0  34863  eulerpartlems  34926  eulerpartlemgf  34945  probmeasb  34996  dfscott2  35672  dfscott3  35673  acycgr2v  35836  cvmliftlem5  35975  bcneg1  36422  wsuceq3  36501  fullfunfv  36633  finminlem  37028  nn0prpwlem  37032  regsfromunir1  37250  bj-ceqsalg0  37722  bj-ceqsalgALT  37724  bj-ceqsalgvALT  37726  bj-vtoclgfALT  37894  finxpreclem4  38237  sin2h  38453  cos2h  38454  tan2h  38455  poimirlem1  38459  poimirlem2  38460  poimirlem3  38461  poimirlem4  38462  poimirlem6  38464  poimirlem7  38465  poimirlem11  38469  poimirlem12  38470  poimirlem16  38474  poimirlem17  38475  poimirlem19  38477  poimirlem20  38478  poimirlem23  38481  poimirlem30  38488  poimirlem32  38490  poimir  38491  broucube  38492  mblfinlem1  38495  mblfinlem3  38497  mblfinlem4  38498  ismblfin  38499  volsupnfl  38503  iblmulc2nc  38523  ftc1anc  38539  dvasin  38542  heiborlem3  38667  heiborlem6  38670  heiborlem8  38672  cdleme32fva  41414  isnumbasgrplem1  44046  areaquad  44161  binomcxplemnotnn0  45284  permaxun  45938  fourierdlem101  47139  fourierdlem103  47141  fourierdlem104  47142  sqwvfourb  47161  fourierswlem  47162  fouriersw  47163  m1mod0mod1  48352  sgoldbeven3prm  48803  pgnbgreunbgrlem2lem1  49134  pgnbgreunbgrlem2lem2  49135  pgnbgreunbgrlem2lem3  49136  iooii  49948  aacllem  50861