Theorem mp3an3 1180

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

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858

This theorem is referenced by:  mp3an13 1182  mp3an23 1183  mp3anl3 1187  fr2nr 3635  fr3nr 3859  funpr 4467  fprOLD 4811  oprabval 4952  oprabvali 4954  oprabval2 4957  ovmpt2 5017  curry1 5075  curry2 5078  oaword1 5234  oneo 5260  oeoalem 5271  oeoelem 5273  mapxpen 5589  nnaun 6089  prlem934b 6290  addcaniOLD 6506  ltxr 6664  xrre 6744  xrre2 6745  mulcani 6878  receui 6890  nnaddcl 7123  nnmulcl 7124  nnge1 7126  nnleltp1 7138  nnltp1le 7139  2halves 7225  halfaddsub 7227  addltmul 7229  nn0leltp1 7337  nn0ltlem1 7338  zleltp1 7391  zextlt 7402  uzindOLD 7420  znq 7438  qbtwnre 7459  qbtwnxr 7460  fraclt1 7470  flhalf 7487  elioc2 7558  elico2 7559  elicc2 7560  icoshftf1oii 7578  eluzp1p1 7604  uzaddcl 7618  fzshftral 7701  shftval3 7761  seqzp1 7791  seqzval2 7796  expadd 7839  expmul 7840  expubnd 7853  sqmul 7857  bernneq 7898  bernneqOLD 7899  sqrlem6 7928  recj 8068  ser1absdiflem 8181  faclbnd2 8198  faclbnd6 8206  fsumrev 8289  fsumshft 8291  serzmulci 8318  binomlem1 8326  binomlem2 8327  climmullem5 8384  caucvglem5 8421  cvgcmp2lem 8440  geoseri 8496  cvgratlem1 8512  ivthlem7 8549  efcltlem1 8566  efaddlem23 8622  efexp 8634  efival 8712  sin01bndlem2 8734  cos01bndlem2 8736  sin01gt0 8742  cos01gt0 8743  znnen 8771  lpval 9019  lpsscls 9021  ioo2bl 9190  bcthlem1 9277  bcthlem33 9309  gx0 9384  gx1 9385  gxm1 9391  gxnn0add 9397  gxnn0mul 9400  sm1cnilem 9686  ip1cnilem5 9716  nvcnpi3 9761  nvcnpi4 9762  ipasslem1 9831  ipasslem2 9832  ipasslem11 9841  minveclem27 9916  sincosq1eq 10059  sineq0 10065  sineq0OLD 10066  efif1lem4 10087  hausfillim 10303  comptoppr 10332  projlem28 10846  pjthlem7 10858  shsva 10917  h1datomi 11137  lnfnmuli 11610  leopsq 11700  nmopleid 11710  opsqrlem3 11713  opsqrlem6 11716  pjnmopi 11719  hstle 11802  csmdsymi 11906  atcvatlem 11957  bnj1260 13019  nn0seqcvgd 13659  divalglem5 13700  algrf 13739  altopelaltxp 14099  hmphsyma 14882  mslb1 15007  msra3 15009  fictblem 15370  ntrin 15411  conntoppr 15445  reconnlem1 15446  tailfb 15639  filnetlem5 15644  filnet 15645  oprabval2a 15707  eroprv 15734  neificl 15841  mettrifi2 15848  oprpiece1res1 15880  oprpiece1res2 15881  txopn 15913  phtpyco 16056  pcoval 16073  igenidl 16211

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 164  df-an 242  df-3an 860

Copyright terms: Public domain