Theorem mp3an1 905

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

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

This theorem is referenced by:  mp3an12 908  mp3an1i 911  mp3anl1 912  mp3an 918  onint 3013  brelrn 3351  tfrlem9 3926  ndmoprcl 4051  oaord1 4192  oaword2 4194  oawordeulem 4195  oa00 4200  omword1 4211  omword2 4212  omlimcl 4216  unfilem2 4563  fodomb 4817  brdom3 4818  brdom7disj 4821  brdom6disj 4822  mulclpi 5040  mulidpq 5088  halfpq 5101  cnegext 5367  negeu 5374  muladd11t 5441  xrre2t 5589  ltaddpost 5670  addge01t 5691  receu 5720  recclt 5734  div0t 5775  recdiv2t 5805  rerecclt 5812  ltmul12it 5850  lemul12itOLD 5852  lemul12it 5853  mulgt1t 5854  lediv12it 5905  ledivp1t 5914  nngt1ne1t 5953  nnaddm1clt 5967  8th4div3 6040  infm3 6063  infmrcl 6078  xrub 6089  supxrre 6092  nn0ltp1let 6136  gtndivt 6202  nn0ind 6221  qbtwnxr 6287  qsqueeze 6288  om2uzran 6308  ser1mono 6345  ndmioo 6378  elioo3g 6388  elioc2t 6398  elico2t 6399  elicc2t 6400  elfz2t 6480  elfz2nn0t 6503  expubndt 6616  le2sqit 6640  bernneq 6660  sqr2irr 6737  imret 6781  cau4i 6925  cau5 6926  cvg3 6930  faclbnd5 6960  fsumcom 7035  climubi 7160  climsup 7162  caucvglem6 7169  caucvg 7170  serzf0 7176  cvgcmp 7191  cvgcmpub 7192  isumnn0nn 7214  geoser 7241  georeclim 7247  geoisumr 7250  0.999... 7253  cvgratlem4 7260  efcltlem1 7311  erelem3 7328  efaddlem6 7350  efaddlem15 7359  ef01tllem2 7391  ef01tllem2OLD 7392  effsumle 7404  efi4pt 7442  cos2tt 7470  cos2tsint 7471  sin01bndlem3 7477  cos01bndlem3 7479  sin01gt0 7484  cos01gt0 7485  demoivre 7492  znnen 7510  infpn2 7517  iooretop 7663  metxplem1 7830  metxplem2 7831  metxplem3 7832  metxp 7838  bl2in 7847  methausi 7885  xplmi 7977  xpcn 7980  bcthlem3 8005  bcthlem9 8011  bcthlem20 8022  bcthlem21 8023  bcthlem24 8026  bcthlem25 8027  isgrpi 8046  ghgrpilem3 8138  ghgrpilem4 8139  ghsubgi 8141  imsmetlem 8326  nmcnilem 8340  va1cnlem 8348  sm1cnilem 8350  ipval2 8360  ip1cnilem2 8377  ip1cnilem3 8378  ip1cnilem5 8380  ip1cnilem6 8381  lnocoi 8421  nmlno0lem 8456  nmblolbii 8462  blometi 8466  blocnilem 8467  blocni 8468  ipasslem1 8493  ipasslem2 8494  ipasslem4 8496  ipasslem5 8497  ipasslem8 8500  ipblnfi 8519  ip2eqi 8520  ubthlem6 8537  ubthlem7 8538  ubthlem8 8539  ubthlem9 8540  ubthlem10 8541  ubthlem11 8542  ubthlem12 8543  ubthlem13 8544  ubthlem14 8545  minveclem9 8556  minveclem15 8562  minveclem16 8563  minveclem18 8565  minveclem19 8566  minveclem21 8568  minveclem25 8572  minveclem27 8574  minveclem28 8575  minveclem30 8577  minveclem31 8578  minveclem35 8582  minveclem36 8583  minveclem37 8584  minveclem38 8585  minveceu 8586  htthlem6 8628  htthlem10 8632  sincosq1eq 8711  efghgrpilem 8721  efifolem5 8728  shftefif1olem 8743  logeftb 8766  h2hmetdval 8850  axhvcom 8855  axhis1 8866  axhis4 8869  hvm1negt 8903  hvsub4t 8908  hvsubdistr2t 8919  hv2timest 8930  hvsubcant 8943  hvsubcan2t 8944  his2subt 8960  his6t 8967  norm-it 8998  normpyct 9015  hhip 9046  hhph 9047  hhcms 9074  hhssabl 9134  hhssnv 9136  hhshsslem2 9140  hhssmetdval 9151  hhsscms 9152  projlem26 9213  projlem30 9217  shscl 9283  shunss 9339  h1datom 9506  osumlem6 9585  homulid2t 9728  honegdit 9737  ho2timest 9747  nmopge0t 9837  nmopgt0t 9838  nmfnge0t 9853  lnopadd 9897  lnopmul 9898  lnopsub 9900  hmopbdopHIL 9914  nmbdoplb 9951  nmcoplb 9960  nmophm 9963  lnopcon 9965  lnfnadd 9974  lnfnsub 9977  nmbdfnlb 9980  nmcfnlb 9989  lnfncon 9992  cnlnadjlem2 10003  cnlnadjlem7 10008  adjbdlnt 10018  nmoptri 10029  nmopco 10030  adjco 10035  nmopcoadj 10036  bracnlnvalt 10049  leopmult 10069  hmopidmchlem 10080  hmopidmpj 10082  pjima 10106  sto2 10167  atcveq0 10278  atcv0eq 10309  atoml 10312  atcvat 10316  atcvat3 10326  ghomgrpilem2 10389  ghomsn 10391  cayleylem2 10413  nndivlub 10425  clsrebb 10487  hmeogrp 10532

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 779

Copyright terms: Public domain