Theorem mp3an1 899

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 831	. 2 |- ((ph /\ (ps /\ ch)) -> th)
4	1, 3	mpan 692	1 |- ((ps /\ ch) -> th)

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

This theorem is referenced by:  mp3an12 902  mp3an1i 905  mp3anl1 906  mp3an 912  onint 2969  tfrlem9 3858  oaord1 4123  oaword2 4125  oawordeulem 4126  oa00 4131  omword1 4142  omword2 4143  omlimcl 4147  unfilem2 4477  fodomb 4724  brdom3 4725  brdom7disj 4728  brdom6disj 4729  mulclpi 4944  mulidpq 4992  halfpq 5005  cnegext 5271  negeu 5278  muladd11t 5345  xrre2t 5494  ltaddpost 5575  addge01t 5596  receu 5621  recclt 5635  div0t 5674  recdiv2t 5703  rerecclt 5710  ltmul12it 5748  lemul12itOLD 5750  lemul12it 5751  mulgt1t 5752  lediv12it 5795  ledivp1t 5804  nngt1ne1t 5843  nnaddm1clt 5856  8th4div3 5929  infm3 5952  infmrcl 5967  xrub 5978  supxrre 5981  nn0ltp1let 6025  gtndivt 6091  nn0ind 6111  qbtwnxr 6168  qsqueeze 6169  om2uzran 6188  ser1mono 6225  elioc2t 6273  elico2t 6274  elicc2t 6275  elfz2nn0t 6378  expubndt 6490  le2sqit 6514  bernneq 6534  sqr2irr 6610  imret 6661  cau4i 6806  cau5 6807  cvg3 6811  faclbnd5 6841  fsumcom 6917  climubi 7040  climsup 7042  caucvglem6 7049  caucvg 7050  serzf0 7056  cvgcmp 7071  cvgcmpub 7072  isumnn0nn 7093  geoser 7120  georeclim 7126  geoisumr 7129  0.999... 7132  cvgratlem4 7139  efcltlem1 7197  erelem3 7214  efaddlem6 7236  efaddlem15 7245  ef01tllem2 7277  effsumle 7289  efi4pt 7328  cos2tt 7356  sin01bndlem3 7362  cos01bndlem3 7364  sin01gt0 7369  cos01gt0 7370  demoivre 7377  znnen 7396  infpn2 7403  iooretop 7552  metxplem1 7714  metxplem2 7715  metxplem3 7716  metxp 7722  bl2in 7731  methausi 7768  xplmi 7855  xpcn 7858  bcthlem3 7883  bcthlem9 7889  bcthlem20 7900  bcthlem21 7901  bcthlem24 7904  bcthlem25 7905  isgrpi 7924  ghgrpilem3 8020  ghgrpilem4 8021  ghsubgi 8023  imsmetlem 8198  nmcnilem 8209  va1cnlem 8214  sm1cnilem 8216  ipval2 8226  ip1cnilem2 8243  ip1cnilem3 8244  ip1cnilem5 8246  ip1cnilem6 8247  lnocoi 8287  nmlno0lem 8320  nmblolbii 8325  blometi 8329  blocnilem 8330  blocni 8331  ipasslem1 8356  ipasslem2 8357  ipasslem4 8359  ipasslem5 8360  ipasslem8 8363  ipblnfi 8382  ip2eqi 8383  ubthlem6 8400  ubthlem7 8401  ubthlem8 8402  ubthlem9 8403  ubthlem10 8404  ubthlem11 8405  ubthlem12 8406  ubthlem13 8407  ubthlem14 8408  minveclem9 8419  minveclem15 8425  minveclem16 8426  minveclem18 8428  minveclem19 8429  minveclem21 8431  minveclem25 8435  minveclem27 8437  minveclem28 8438  minveclem30 8440  minveclem31 8441  minveclem35 8445  minveclem36 8446  minveclem37 8447  minveclem38 8448  minveceu 8449  htthlem6 8489  htthlem10 8493  sincosq1eq 8539  efghgrpilem 8547  efifolem5 8554  shftefif1olem 8574  shftefif1olemOLD 8575  logeftb 8599  logeftbOLD 8619  ghomgrpilem2 8653  ghomsn 8655  cayleylem2 8677  hvm1negt 9050  hvsub4t 9055  hvsubdistr2t 9066  hv2timest 9077  hvsubcant 9090  hvsubcan2t 9091  his2subt 9107  his6t 9114  norm-it 9145  normpyct 9162  hhmetdval 9192  hhip 9193  hhph 9194  hhcms 9223  projlem26 9341  projlem30 9345  shscl 9410  shunss 9466  h1datom 9635  osumlem6 9714  homulid2t 9857  honegdit 9866  ho2timest 9876  nmopge0t 9965  nmopgt0t 9966  nmfnge0t 9981  lnopadd 10025  lnopmul 10026  lnopsub 10028  hmopbdopHIL 10042  nmbdoplb 10078  nmcoplb 10087  nmophm 10090  lnopcon 10092  lnfnadd 10101  lnfnsub 10104  nmbdfnlb 10107  nmcfnlb 10116  lnfncon 10119  cnlnadjlem2 10130  cnlnadjlem7 10135  adjbdlnt 10145  nmoptri 10155  nmopco 10156  adjco 10161  nmopcoadj 10162  leopmult 10193  hmopidmchlem 10203  hmopidmpj 10205  pjima 10229  sto2 10288  atcveq0 10397  atcv0eq 10428  atoml 10431  atcvat 10435  atcvat3 10445

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 774

Copyright terms: Public domain