Theorem jctil 306

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  jctl  308  ddifnel  3132  unidif  3691  iunxdif2  3784  exss  4063  reg2exmidlema  4363  limom  4441  xpiindim  4586  relssres  4763  funco  5067  nfunsn  5351  fliftcnv  5588  fo1stresm  5946  fo2ndresm  5947  dftpos3  6041  tfri1d  6114  rdgtfr  6153  rdgruledefgg  6154  frectfr  6179  elixpsn  6506  mapxpen  6618  phplem2  6623  sbthlem2  6721  sbthlemi3  6722  djuss  6815  caseinl  6836  exmidfodomrlemr  6889  exmidfodomrlemrALT  6890  nqprrnd  7163  nqprxx  7166  ltexprlempr  7228  recexprlempr  7252  cauappcvgprlemcl  7273  caucvgprlemcl  7296  caucvgprprlemcl  7324  lemulge11  8388  nn0ge2m1nn  8794  frecfzennn  9894  demoivreALT  11124  topcld  11870