Theorem mpanl12 718

Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)

Hypotheses

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

Assertion

Ref	Expression
mpanl12	|- ( ch -> th )

Proof of Theorem mpanl12

Step	Hyp	Ref	Expression
1		mpanl12.2	. 2 |- ps
2		mpanl12.1	. . 3 |- ph
3		mpanl12.3	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	2, 3	mpanl1 716	. 2 |- ( ( ps /\ ch ) -> th )
5	1, 4	mpan 706	1 |- ( ch -> th )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  reuun1  3909  frminex  5094  tz6.26i  5712  wfii  5714  opthreg  8515  unsnen  9375  axcnre  9985  addgt0  10514  addgegt0  10515  addgtge0  10516  addge0  10517  addgt0i  10567  addge0i  10568  addgegt0i  10569  add20i  10571  mulge0i  10575  recextlem1  10657  recne0  10698  recdiv  10731  rec11i  10766  recgt1  10919  prodgt0i  10930  prodge0i  10931  xadddi2  12127  iccshftri  12307  iccshftli  12309  iccdili  12311  icccntri  12313  mulexpz  12900  expaddz  12904  m1expeven  12907  iexpcyc  12969  cnpart  13980  resqrex  13991  sqreulem  14099  amgm2  14109  rlim  14226  ello12  14247  elo12  14258  efcllem  14808  ege2le3  14820  dvdslelem  15031  divalglem1  15117  divalglem6  15121  divalglem9  15124  gcdaddmlem  15245  sqnprm  15414  prmlem1  15814  prmlem2  15827  xpscfn  16219  m1expaddsub  17918  psgnuni  17919  gzrngunitlem  19811  lmres  21104  zdis  22619  iihalf1  22730  lmclimf  23102  vitali  23382  ismbf  23397  ismbfcn  23398  mbfconst  23402  cncombf  23425  cnmbf  23426  limcfval  23636  dvnfre  23715  quotlem  24055  ulmval  24134  ulmpm  24137  abelthlem2  24186  abelthlem3  24187  abelthlem5  24189  abelthlem7  24192  efcvx  24203  logtayl  24406  logccv  24409  cxpcn3  24489  emcllem2  24723  zetacvg  24741  basellem5  24811  bposlem7  25015  chebbnd1lem3  25160  dchrisumlem3  25180  iscgrgd  25408  axcontlem2  25845  nv1  27530  blocnilem  27659  ipasslem8  27692  siii  27708  ubthlem1  27726  norm1  28106  hhshsslem2  28125  hoscli  28621  hodcli  28622  cnlnadjlem7  28932  adjbdln  28942  pjnmopi  29007  strlem1  29109  rexdiv  29634  tpr2rico  29958  qqhre  30064  signsply0  30628  subfacval3  31171  erdszelem4  31176  erdszelem8  31180  elmrsubrn  31417  rdgprc  31700  frindi  31741  fwddifval  32269  fwddifnval  32270  poimirlem29  33438  ismblfin  33450  itg2addnclem  33461  caures  33556