Theorem simpl2im 390

Description: Implication from an eliminated conjunct implied by the antecedent. (Contributed by BJ/AV, 5-Apr-2021.)

Hypotheses

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

Assertion

Ref	Expression
simpl2im	|- ( ph -> th )

Proof of Theorem simpl2im

Step	Hyp	Ref	Expression
1		simpl2im.1	. 2 |- ( ph -> ( ps /\ ch ) )
2		simpr 110	. 2 |- ( ( ps /\ ch ) -> ch )
3		simpl2im.2	. 2 |- ( ch -> th )
4	1, 2, 3	3syl 17	1 |- ( ph -> th )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107

This theorem is used by:  rabsnif  3778  ctssdccl  7458  enumct  7462  djuen  7574  ndvdssub  12722  sgrpidmndm  13792  conjsubgen  14140  cntzssv  14160  cntzi  14162  xmeteq0  15618  xmettri2  15620  metcnpi  15774  metcnpi2  15775  dvbssntrcntop  15943  upgrm  16579  umgrpredgv  16626