Theorem jctil 305

Description: Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.)

Hypotheses

Ref	Expression
jctil.1	|- ( ph -> ps )
jctil.2	|- ch

Assertion

Ref	Expression
jctil	|- ( ph -> ( ch /\ ps ) )

Proof of Theorem jctil

Step	Hyp	Ref	Expression
1		jctil.2	. . 3 |- ch
2	1	a1i 9	. 2 |- ( ph -> ch )
3		jctil.1	. 2 |- ( ph -> ps )
4	2, 3	jca 300	1 |- ( ph -> ( ch /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106

This theorem is referenced by:  jctl  307  ddifnel  3104  unidif  3641  iunxdif2  3734  exss  3990  reg2exmidlema  4285  limom  4362  xpiindim  4501  relssres  4676  funco  4970  nfunsn  5239  fliftcnv  5466  fo1stresm  5819  fo2ndresm  5820  dftpos3  5911  tfri1d  5984  rdgtfr  6023  rdgruledefgg  6024  frectfr  6049  phplem2  6388  nqprrnd  6795  nqprxx  6798  ltexprlempr  6860  recexprlempr  6884  cauappcvgprlemcl  6905  caucvgprlemcl  6928  caucvgprprlemcl  6956  lemulge11  8011  nn0ge2m1nn  8415  frecfzennn  9508