Theorem mp3an2 901

Description: An inference based on modus ponens.

Hypotheses

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

Assertion

Ref	Expression
mp3an2	|- ((ph /\ ch) -> th)

Proof of Theorem mp3an2

Step	Hyp	Ref	Expression
1		mp3an2.1	. 2 |- ps
2		mp3an2.2	. . 3 |- ((ph /\ ps /\ ch) -> th)
3	2	3expa 831	. 2 |- (((ph /\ ps) /\ ch) -> th)
4	1, 3	mpanl2 705	1 |- ((ph /\ ch) -> th)

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

This theorem is referenced by:  mp3anl2 908  elabgt 1886  tz7.7 2963  ordin 2967  onfr 2976  tfrlem11 3906  htalem 4699  ac6lem 4726  zorn2lem1 4760  uniimadom 4782  muladd11t 5394  nncant 5441  muleqaddt 5669  diveq0t 5724  nnsub 5903  avglet 5991  nnunb 6017  supxrbnd 6038  zltp1let 6128  zbtwnre 6169  rebtwnz 6170  fladdzt 6187  eluzp1m1t 6365  seqzp1 6480  expnbndt 6585  leabst 6799  abs2dift 6839  cau5i 6854  cvg3 6860  caubnd 6863  faclbnd2 6883  faclbnd3 6884  faclbnd5 6890  bcn0t 6901  bcnnt 6902  bcnp11t 6903  bcnp1nt 6904  bccl2t 6909  fsumshft 6969  fsumconst 6976  binomlem1 7004  binomlem2 7005  climshft 7041  iserzshft2 7044  climcau 7092  serzf0 7105  ser1f0 7106  georeclim 7175  geoisum1c 7180  fsum0diaglem2 7192  fsum0diag4 7196  ivthlem6 7221  ivthlem7 7222  ivthlem6OLD 7230  ivthlem7OLD 7231  cos2tt 7405  sin01bndlem2 7410  cos01bndlem2 7412  sin01gt0 7418  cos01gt0 7419  demoivre 7426  demoivreALT 7427  nn0ennn 7439  znnenlem 7443  znnenlemOLD 7444  subtop 7588  lmuni 7886  metelcls 7900  metcn4i 7906  iscms2lem4 7926  vc0 8125  vcm 8127  vcnegsubdi2 8131  vcsub4 8132  invfval 8201  nvzs 8205  nvmf 8206  nvmdi 8210  nvnegneg 8211  nvsubadd 8215  nvpncan2 8216  nvaddsub4 8221  nvnncan 8223  nvm1 8231  nvdif 8232  nvpi 8233  nvz0 8235  nvmtri 8238  nvabs 8240  nvge0 8241  imsmetlem 8261  nvlmcl 8267  sm1cnilem 8281  4ipval2 8292  ipval3 8293  ipid 8297  ipcj 8301  sspmval 8326  ipasslem1 8421  ipasslem2 8422  ipsubdir 8439  pilem1 8590  hvsubdistr1t 8837  shsubclt 9010  occllem6 9094  projlem26 9127  shsel3t 9194  shunss 9252  hosubdit 9651  lnopm 9840  nmophm 9876  nmopco 9942  hmopidmch 9990  hstlet 10067  hst0t 10070  stadd 10083  mdsl2 10157  superpos 10189  dmdbr5at 10255

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 775

Copyright terms: Public domain