Theorem jctil 312

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  jctl  314  ddifnel  3266  unidif  3840  iunxdif2  3933  exss  4225  reg2exmidlema  4531  limom  4611  xpiindim  4761  relssres  4942  funco  5253  nfunsn  5546  fliftcnv  5791  fo1stresm  6157  fo2ndresm  6158  dftpos3  6258  tfri1d  6331  rdgtfr  6370  rdgruledefgg  6371  frectfr  6396  elixpsn  6730  mapxpen  6843  phplem2  6848  sbthlem2  6952  sbthlemi3  6953  djuss  7064  caseinl  7085  caseinr  7086  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  2omotaplemap  7251  nqprrnd  7537  nqprxx  7540  ltexprlempr  7602  recexprlempr  7626  cauappcvgprlemcl  7647  caucvgprlemcl  7670  caucvgprprlemcl  7698  suplocsrlempr  7801  lemulge11  8817  nn0ge2m1nn  9230  frecfzennn  10419  reccn2ap  11312  demoivreALT  11772  pcdiv  12292  topcld  13391  metrest  13788  pwle2  14519