Theorem mp3an1 1025

Description: An inference based on modus ponens.

Hypotheses

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

Assertion

Ref	Expression
mp3an1	|- ((ps /\ ch) -> th)

Proof of Theorem mp3an1

Step	Hyp	Ref	Expression
1		mp3an1.1	. 2 |- ph
2		mp3an1.2	. . 3 |- ((ph /\ ps /\ ch) -> th)
3	2	3expb 947	. 2 |- ((ph /\ (ps /\ ch)) -> th)
4	1, 3	mpan 756	1 |- ((ps /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 239   /\ w3a 855

This theorem is referenced by:  mp3an12 1028  mp3an1i 1031  mp3anl1 1032  mp3an 1038  onint 3687  brelrn 4002  ndmoprcl 4788  tfrlem9 4938  oaord1 5044  oaword2 5046  oawordeulem 5047  oa00 5052  omword1 5063  omword2 5064  omlimcl 5068  oeoelem 5084  unfilem2 5452  fodomb 5758  brdom3 5759  brdom7disj 5762  brdom6disj 5763  mulclpi 5969  mulidpq 6017  halfpq 6030  cnegex 6298  negeui 6306  muladd11 6380  xrre2 6541  ltaddpos 6635  addge01 6657  reccl 6700  div0 6739  rec11r 6751  divdiv23zi 6766  recdiv2 6769  rereccl 6776  ltmul12a 6818  lemul12aOLD 6820  lemul12a 6821  mulgt1 6822  ltdiv23i 6872  lediv12a 6874  ledivp1 6883  ltdivp1i 6885  nngt1ne1 6922  nnaddm1cl 6937  8th4div3 7012  infm3 7058  infmrcl 7073  xrub 7084  supxrre 7087  nn0ltp1le 7131  gtndiv 7200  nn0ind 7219  qbtwnxr 7255  qsqueeze 7256  ndmioo 7332  elioo3g 7342  elioc2 7353  elico2 7354  elicc2 7355  elfz2 7437  elfz2nn0 7462  om2uzrani 7506  cardfz 7514  ser1monoi 7545  expordi 7640  expubnd 7648  le2sq2 7672  bernneq 7693  bernneqOLD 7694  sqr2irr 7774  imre 7818  mulre 7822  absdivzi 7905  cau4ii 7965  cau5i 7966  cvg3i 7970  faclbnd5 8000  fsumcom 8083  climubii 8208  climsupi 8210  caucvglem6 8217  caucvgi 8218  serzf0i 8224  cvgcmpi 8240  cvgcmpubi 8241  isumnn0nn 8263  geoseri 8291  georeclim 8297  geoisumr 8300  0.999... 8303  cvgratlem4 8310  efcltlem1 8361  erelem3 8378  efaddlem5 8399  efaddlem6 8400  efaddlem15 8409  efsub 8428  ef01tllem2 8441  ef01tllem2OLD 8442  effsumlei 8457  reeff1o 8486  efi4p 8495  cos2t 8523  cos2tsin 8524  sin01bndlem3 8530  cos01bndlem3 8532  sin01gt0 8537  cos01gt0 8538  absefib 8545  efieq1re 8546  demoivre 8547  infpn2 8573  iooretop 8724  metxplem1 8898  metxplem2 8899  metxplem3 8900  metxp 8906  bl2in 8915  methausi 8954  xplmi 9046  xpcn 9049  bcthlem3 9074  bcthlem9 9080  bcthlem20 9091  bcthlem21 9092  bcthlem24 9095  bcthlem25 9096  isgrpi 9117  ghgrpilem3 9238  ghgrpilem4 9239  ghsubgi 9241  imsmetlem 9450  vacnlem3 9464  nmcnilem 9471  va1cnlem 9479  sm1cnilem 9481  ipval2 9491  ip1cnilem2 9508  ip1cnilem3 9509  ip1cnilem5 9511  ip1cnilem6 9512  lnocoi 9552  nmlno0lem 9588  nmblolbii 9594  blometi 9598  blocnilem 9599  blocni 9600  ipasslem1 9626  ipasslem2 9627  ipasslem4 9629  ipasslem5 9630  ipasslem8 9633  ipblnfi 9652  ip2eqi 9653  ubthlem6 9672  ubthlem7 9673  ubthlem8 9674  ubthlem9 9675  ubthlem10 9676  ubthlem11 9677  ubthlem12 9678  ubthlem12OLD 9679  ubthlem13 9680  ubthlem13OLD 9681  ubthlem14 9682  minveclem9 9693  minveclem15 9699  minveclem16 9700  minveclem18 9702  minveclem19 9703  minveclem21 9705  minveclem25 9709  minveclem27 9711  minveclem28 9712  minveclem30 9714  minveclem31 9715  minveclem35 9719  minveclem36 9720  minveclem37 9721  minveclem38 9722  minveceu 9723  htthlem6 9767  htthlem10 9771  sincosq1eq 9854  efghgrpilem 9868  efifolem5 9875  shftefif1olem 9890  logeftb 9913  h2hmetdval 10272  axhvcom 10277  axhis1 10288  axhis4 10291  hvm1neg 10325  hvsub4 10330  hvsubdistr2 10341  hv2times 10352  hvsubcan 10366  hvsubcan2 10367  his2sub 10383  his6 10390  norm-i 10421  normpyc 10438  hhip 10469  hhph 10470  hhcms 10497  hhssabli 10557  hhssnv 10559  hhshsslem2 10563  hhssmetdval 10574  hhsscms 10575  projlem26 10636  projlem30 10640  shscli 10706  shunssi 10762  h1datomi 10929  osumlem6 11010  homulid2 11155  honegdi 11164  ho2times 11174  eigrei 11189  nmopge0 11264  nmopgt0 11265  nmfnge0 11280  lnopaddi 11324  lnopmuli 11325  lnopsubi 11327  hmopbdopiHIL 11341  nmbdoplbi 11378  nmcoplbi 11387  nmophmi 11390  lnopconi 11392  lnfnaddi 11401  lnfnsubi 11404  nmbdfnlbi 11407  nmcfnlbi 11416  lnfnconi 11419  cnlnadjlem2 11430  cnlnadjlem7 11435  adjbdln 11445  nmoptrii 11456  nmopcoi 11457  adjcoi 11462  nmopcoadji 11463  bracnlnval 11477  leopmul 11497  opsqrlem1 11503  opsqrlem6 11508  hmopidmchlem 11514  hmopidmpji 11516  pjimai 11540  sto2i 11601  atcveq0 11712  atcv0eq 11743  atomli 11746  atcvati 11750  atcvat3i 11760  bnj221 12304  fnn0ind 13403  ghomgrpilem2 13421  ghomsn 13423  cayleylem2 13434  supminf 13448  divalglem0 13488  divalglem4 13491  divalglem5 13492  divalglem9 13496  gcdcllem3 13512  gcdn0gt0 13520  algcvg 13536  algcvgblem 13537  algcvga 13539  mulgcdlem2 13549  mulgcdlem3 13550  zgt1b1 13563  isprm3 13568  coprm 13574  wfrlem12 13760  nndivlub 13989  clsrebb 14567  hmeogrp 14612  reconnlem1 15128  fneer 15178  lincmb01cmp 15560  txmet 15607  heiborlem16 15652  heiborlem32 15668  heiborlem36 15672  heiborlem37 15673  bfplem8 15687  bfplem9 15688  bfplem11 15690  rrncms 15701  phtpyid 15731  phtpycom 15732  phtpycolem3 15735  phtpycolem4 15736  phtpycolem5 15737  reparpht 15747  pcocn 15758  pcohtpylem3 15764  pcopt 15766  pcorevlem 15768  pcorev 15769  pi1gp 15777

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 163  df-an 241  df-3an 857

Copyright terms: Public domain