Theorem mpanl12 773

Description: An inference based on modus ponens.

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 770	. 2 |- ((ps /\ ch) -> th)
5	1, 4	mpan 759	1 |- (ch -> th)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  reuun1 2872  opthreg 5709  unsnen 5985  cdaun 6070  cdacomen 6079  addgt0 6831  addgegt0 6833  addgtge0 6835  addge0 6837  divadddivi 6965  recdiv 6967  recgt0 7043  recgt1 7082  8th4div3 7217  exprec 7837  exple1 7852  crreczi 7991  climunii 8358  serzf0i 8429  iserzabslem 8438  cvgcmp2clem 8442  efcltlem1 8566  efaddlem25 8624  ef1tllem 8643  efgt0i 8669  sin01bndlem3 8735  opr1cn 9256  opr2cn 9257  grpidinv2 9344  grpinv 9353  nv1 9636  blocni 9805  siii 9854  ubthlem8 9879  ubthlem12 9883  ubthlem12OLD 9884  ubthlem13 9885  ubthlem13OLD 9886  minveclem9 9898  minveclem16 9905  minveclem21 9910  minveclem25 9914  minveclem28 9917  minveclem35 9924  minveclem37 9926  minveclem38 9927  cosh111lem1 10068  hlimuniii 10741  norm1 10754  hhshsslem2 10771  projlem2 10820  projlem28 10846  pjcompi 11254  hoscli 11325  hodcli 11326  hoaddcomi 11335  hodsi 11338  hoaddassi 11339  hocadddiri 11342  hocsubdiri 11343  hoddii 11551  lnophsi 11563  nmcopexlem5 11592  nmcfnexlem5 11621  nmoptrii 11664  pjnmopi 11719  pjsdii 11727  pjddii 11728  pjscji 11742  pjtoi 11751  strlem1 11822  dvdslelem 13692  divalglem1 13697  divalglem6 13701  divalglem9 13704  gcdaddmlem 13734  tz6.26i 13914  frminex 15773  iccshftri 15858  iccshftli 15860  iccdili 15862  icccntri 15864  iihalf1 15872  lincmb01cmp 15878  grpidinv2NEW 17119  grpinvNEW 17128

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 164  df-an 242

Copyright terms: Public domain