Theorem mp3an2 902

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 832	. 2 |- (((ph /\ ps) /\ ch) -> th)
4	1, 3	mpanl2 706	1 |- ((ph /\ ch) -> th)

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

This theorem is referenced by:  mp3anl2 909  elabgt 1891  tz7.7 2968  ordin 2972  onfr 2981  tfrlem11 3912  htalem 4707  ac6lem 4734  zorn2lem1 4768  uniimadom 4790  muladd11t 5402  nncant 5449  muleqaddt 5677  diveq0t 5732  nnsub 5911  avglet 5999  nnunb 6025  supxrbnd 6046  zltp1let 6136  zbtwnre 6177  rebtwnz 6178  fladdzt 6195  eluzp1m1t 6373  seqzp1 6488  expnbndt 6593  leabst 6807  abs2dift 6847  cau5i 6862  cvg3 6868  caubnd 6871  faclbnd2 6891  faclbnd3 6892  faclbnd5 6898  bcn0t 6909  bcnnt 6910  bcnp11t 6911  bcnp1nt 6912  bccl2t 6917  fsumshft 6977  fsumconst 6984  binomlem1 7012  binomlem2 7013  climshft 7049  iserzshft2 7052  climcau 7100  serzf0 7113  ser1f0 7114  georeclim 7183  geoisum1c 7188  fsum0diaglem2 7200  fsum0diag4 7204  ivthlem6 7229  ivthlem7 7230  ivthlem6OLD 7238  ivthlem7OLD 7239  cos2tt 7413  sin01bndlem2 7418  cos01bndlem2 7420  sin01gt0 7426  cos01gt0 7427  demoivre 7434  demoivreALT 7435  nn0ennn 7447  znnenlem 7451  znnenlemOLD 7452  subtop 7596  lmuni 7902  metelcls 7916  metcn4i 7922  iscms2lem4 7942  vc0 8140  vcm 8142  vcnegsubdi2 8146  vcsub4 8147  invfval 8213  nvzs 8217  nvmf 8218  nvmdi 8222  nvnegneg 8223  nvsubadd 8227  nvpncan2 8228  nvaddsub4 8233  nvnncan 8235  nvm1 8244  nvdif 8245  nvpi 8246  nvz0 8248  nvmtri 8251  nvabs 8253  nvge0 8254  imsmetlem 8274  nvlmcl 8280  sm1cnilem 8294  4ipval2 8305  ipval3 8306  ipid 8310  ipcj 8314  sspmval 8339  ipasslem1 8434  ipasslem2 8435  ipsubdir 8452  pilem1 8609  hvsubdistr1t 8855  shsubclt 9028  occllem6 9117  projlem26 9150  shsel3t 9217  shunss 9275  hosubdit 9674  lnopm 9863  nmophm 9899  nmopco 9966  hmopidmch 10017  hstlet 10095  hst0t 10098  stadd 10111  mdsl2 10186  superpos 10218  dmdbr5at 10284

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 776

Copyright terms: Public domain