Theorem mp3an3 903

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 832	. 2 |- (((ph /\ ps) /\ ch) -> th)
4	1, 3	mpan2 695	1 |- ((ph /\ ps) -> th)

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

This theorem is referenced by:  mp3an13 905  mp3an23 906  mp3anl3 910  fr2nr 2920  fr3nr 2921  oprabval 4014  oprabvali 4016  oprabval2 4019  curry1 4088  oaword1 4176  oneo 4202  mapxpen 4481  prlem934b 5118  addcan 5331  ltxrt 5475  xrret 5550  xrre2t 5551  mulcan 5667  nnaddclt 5896  nnmulclt 5897  nnge1t 5899  nnleltp1t 5909  nnltp1let 5910  2halvest 5994  halfaddsubt 5996  nn0leltp1t 6083  nn0ltlem1t 6084  zleltp1t 6137  zextltt 6145  uzindOLD 6164  flhalft 6197  znq 6204  qbtwnre 6224  qbtwnxr 6225  shftval3t 6293  elioc2t 6330  elico2t 6331  elicc2t 6332  icoshftf1oi 6350  eluzp1p1t 6375  uzaddclt 6389  fzshftralt 6462  seqzp1 6488  seqzval2t 6493  expaddt 6535  expmult 6536  expubndt 6547  sqmult 6551  bernneq 6591  sqrlem6 6616  recjt 6761  ser1absdiflem 6874  faclbnd6 6899  fsumrev 6975  fsumshft 6977  serzmulc 7004  binomlem1 7012  binomlem2 7013  climmullem5 7068  caucvglem5 7105  cvgcmp2lem 7124  geoser 7177  cvgratlem1 7193  ivthlem7 7230  ivthlem7OLD 7239  efcltlem1 7254  efexpt 7322  efivalt 7397  sin01bndlem2 7418  cos01bndlem2 7420  sin01gt0 7426  cos01gt0 7427  znnen 7453  lpval 7693  lpsscls 7695  ioo2bl 7864  bcthlem1 7949  bcthlem21 7969  bcthlem33 7981  sm1cnilem 8294  ip1cnilem5 8324  nvcnpi4 8368  ipasslem1 8434  ipasslem2 8435  ipasslem11 8444  minveclem27 8515  sincosq1eq 8645  efif1lem4 8667  projlem28 9152  pjthlem7 9163  shsvat 9222  h1datom 9444  lnfnmul 9911  leopsqt 10000  nmopleidt 10010  pjnmop 10013  hstlet 10095  csmdsym 10198  atcvatlem 10249  hmphsyma 10451

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 776

Copyright terms: Public domain