Theorem mpanl12 708

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  reuun1 2277  opthreg 4604  cdaun 4922  cdacomen 4929  recgt0t 5861  recgt1t 5899  8th4div3 6031  exple1t 6607  crrecz 6741  climunii 7098  serzf0 7169  ser1f0 7170  iserzabslem 7178  efcltlem1 7304  efaddlem25 7362  ef1tllem 7381  efgt0 7404  sin01bndlem3 7469  opr1cn 7978  opr2cn 7979  grpidinv2 8060  grpinv 8069  nv1 8304  blocni 8465  siii 8513  ubthlem8 8536  ubthlem12 8540  ubthlem13 8541  minveclem9 8553  minveclem16 8560  minveclem21 8565  minveclem25 8569  minveclem28 8572  minveclem35 8579  minveclem37 8581  minveclem38 8582  cosh111lem1 8714  hlimunii 9108  norm1t 9121  hhshsslem2 9138  projlem2 9187  projlem28 9213  pjcomp 9619  hoscl 9688  hodcl 9689  hoaddcom 9698  hods 9701  hoaddass 9702  hocadddir 9705  hocsubdir 9706  hoddi 9914  lnophs 9926  nmcopexlem5 9955  nmcfnexlem5 9984  nmoptri 10027  pjnmop 10075  pjsdi 10083  pjddi 10084  pjscj 10098  pjtot 10107  strlem1 10177

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

Copyright terms: Public domain