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	⊢ (𝜑 → 𝜓)
jctil.2	⊢ 𝜒

Assertion

Ref	Expression
jctil	⊢ (𝜑 → (𝜒 ∧ 𝜓))

Proof of Theorem jctil

Step	Hyp	Ref	Expression
1		jctil.2	. . 3 ⊢ 𝜒
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝜒)
3		jctil.1	. 2 ⊢ (𝜑 → 𝜓)
4	2, 3	jca 300	1 ⊢ (𝜑 → (𝜒 ∧ 𝜓))

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  3103  unidif  3633  iunxdif2  3726  exss  3982  reg2exmidlema  4277  limom  4354  xpiindim  4491  relssres  4666  funco  4960  nfunsn  5228  fliftcnv  5455  fo1stresm  5808  fo2ndresm  5809  dftpos3  5900  tfri1d  5972  rdgtfr  5984  rdgruledefgg  5985  frectfr  6008  phplem2  6339  nqprrnd  6733  nqprxx  6736  ltexprlempr  6798  recexprlempr  6822  cauappcvgprlemcl  6843  caucvgprlemcl  6866  caucvgprprlemcl  6894  lemulge11  7944  nn0ge2m1nn  8348  frecfzennn  9419