Theorem mp3an3 902

Description: An inference based on modus ponens.

Hypotheses

Ref	Expression
mp3an3.1	|- ch
mp3an3.2	|- ((ph /\ ps /\ ch) -> th)

Assertion

Ref	Expression
mp3an3	|- ((ph /\ ps) -> th)

Proof of Theorem mp3an3

Step	Hyp	Ref	Expression
1		mp3an3.1	. 2 |- ch
2		mp3an3.2	. . 3 |- ((ph /\ ps /\ ch) -> th)
3	2	3expa 831	. 2 |- (((ph /\ ps) /\ ch) -> th)
4	1, 3	mpan2 694	1 |- ((ph /\ ps) -> th)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 773

This theorem is referenced by:  mp3an13 904  mp3an23 905  mp3anl3 909  fr2nr 2915  fr3nr 2916  oprabval 4008  oprabvali 4010  oprabval2 4013  curry1 4082  oaword1 4170  oneo 4196  mapxpen 4475  prlem934b 5110  addcan 5323  ltxrt 5467  xrret 5542  xrre2t 5543  mulcan 5659  nnaddclt 5888  nnmulclt 5889  nnge1t 5891  nnleltp1t 5901  nnltp1let 5902  2halvest 5986  halfaddsubt 5988  nn0leltp1t 6075  nn0ltlem1t 6076  zleltp1t 6129  zextltt 6137  uzindOLD 6156  flhalft 6189  znq 6196  qbtwnre 6216  qbtwnxr 6217  shftval3t 6285  elioc2t 6322  elico2t 6323  elicc2t 6324  icoshftf1oi 6342  eluzp1p1t 6367  uzaddclt 6381  fzshftralt 6454  seqzp1 6480  seqzval2t 6485  expaddt 6527  expmult 6528  expubndt 6539  sqmult 6543  bernneq 6583  sqrlem6 6608  recjt 6753  ser1absdiflem 6866  faclbnd6 6891  fsumrev 6967  fsumshft 6969  serzmulc 6996  binomlem1 7004  binomlem2 7005  climmullem5 7060  caucvglem5 7097  cvgcmp2lem 7116  geoser 7169  cvgratlem1 7185  ivthlem7 7222  ivthlem7OLD 7231  efcltlem1 7246  efexpt 7314  efivalt 7389  sin01bndlem2 7410  cos01bndlem2 7412  sin01gt0 7418  cos01gt0 7419  znnen 7445  lpval 7684  lpsscls 7686  ioo2bl 7851  bcthlem1 7933  bcthlem21 7953  bcthlem33 7965  sm1cnilem 8281  ip1cnilem5 8311  nvcnpi4 8355  ipasslem1 8421  ipasslem2 8422  ipasslem11 8431  minveclem27 8502  sincosq1eq 8626  efif1lem4 8648  projlem28 9129  pjthlem7 9140  shsvat 9199  h1datom 9421  lnfnmul 9888  leopsqt 9974  nmopleidt 9983  pjnmop 9986  hstlet 10067  csmdsym 10169  atcvatlem 10220  hmphsyma 10415

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 775

Copyright terms: Public domain