Theorem jctil 295

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 290	1 ⊢ (𝜑 → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 97

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

This theorem is referenced by:  jctl  297  ddifnel  3075  unidif  3612  iunxdif2  3705  exss  3963  reg2exmidlema  4259  onpsssuc  4295  limom  4336  xpiindim  4473  relssres  4648  funco  4940  nfunsn  5207  fliftcnv  5435  fo1stresm  5788  fo2ndresm  5789  dftpos3  5877  tfri1d  5949  rdgtfr  5961  rdgruledefgg  5962  frectfr  5985  phplem2  6316  nqprrnd  6641  nqprxx  6644  ltexprlempr  6706  recexprlempr  6730  cauappcvgprlemcl  6751  caucvgprlemcl  6774  caucvgprprlemcl  6802  lemulge11  7832  nn0ge2m1nn  8242  frecfzennn  9203