Theorem mpanl12 707

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  reuun1 2273  opthreg 4584  cdaun 4902  cdacomen 4909  recgt0t 5823  recgt1t 5855  8th4div3 5986  exple1t 6546  crrecz 6680  climunii 7043  serzf0 7113  ser1f0 7114  iserzabslem 7122  efcltlem1 7254  efaddlem25 7312  ef1tllem 7331  efgt0 7353  sin01bndlem3 7419  opr1cn 7928  opr2cn 7929  grpidinv2 8010  grpinv 8019  nv1 8256  blocni 8409  siii 8457  ubthlem8 8480  ubthlem12 8484  ubthlem13 8485  minveclem9 8497  minveclem16 8504  minveclem21 8509  minveclem25 8513  minveclem28 8516  minveclem35 8523  minveclem37 8525  minveclem38 8526  cosh111lem1 8648  hlimunii 9047  norm1t 9060  hhshsslem2 9077  projlem2 9126  projlem28 9152  pjcomp 9559  hoscl 9628  hodcl 9629  hoaddcom 9638  hods 9641  hoaddass 9642  hocadddir 9645  hocsubdir 9646  hoddi 9852  lnophs 9864  nmcopexlem5 9893  nmcfnexlem5 9922  nmoptri 9965  pjnmop 10013  pjsdi 10021  pjddi 10022  pjscj 10036  pjtot 10045  strlem1 10115

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