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  3131  unidif  3685  iunxdif2  3778  exss  4054  reg2exmidlema  4350  limom  4428  xpiindim  4573  relssres  4750  funco  5054  nfunsn  5338  fliftcnv  5574  fo1stresm  5932  fo2ndresm  5933  dftpos3  6027  tfri1d  6100  rdgtfr  6139  rdgruledefgg  6140  frectfr  6165  mapxpen  6564  phplem2  6569  sbthlem2  6667  sbthlemi3  6668  djuss  6761  exmidfodomrlemr  6828  exmidfodomrlemrALT  6829  nqprrnd  7102  nqprxx  7105  ltexprlempr  7167  recexprlempr  7191  cauappcvgprlemcl  7212  caucvgprlemcl  7235  caucvgprprlemcl  7263  lemulge11  8327  nn0ge2m1nn  8733  frecfzennn  9833  demoivreALT  11063