This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem jccil

Description: Inference conjoining a consequent of a consequent to the left of the consequent in an implication. Remark: One can also prove this theorem using syl and jca (as done in jccir ), which would be 4 bytes shorter, but one step longer than the current proof. (Proof modification is discouraged.) (Contributed by AV, 20-Aug-2019)

Ref Expression
Hypotheses jccir.1 
|- ( ph -> ps )
jccir.2 
|- ( ps -> ch )
Assertion jccil 
|- ( ph -> ( ch /\ ps ) )

Proof

Step Hyp Ref Expression
1 jccir.1 
 |-  ( ph -> ps )
2 jccir.2 
 |-  ( ps -> ch )
3 1 2 jccir 
 |-  ( ph -> ( ps /\ ch ) )
4 3 ancomd 
 |-  ( ph -> ( ch /\ ps ) )