Theorem jctil 310

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  jctl  312  ddifnel  3253  unidif  3821  iunxdif2  3914  exss  4205  reg2exmidlema  4511  limom  4591  xpiindim  4741  relssres  4922  funco  5228  nfunsn  5520  fliftcnv  5763  fo1stresm  6129  fo2ndresm  6130  dftpos3  6230  tfri1d  6303  rdgtfr  6342  rdgruledefgg  6343  frectfr  6368  elixpsn  6701  mapxpen  6814  phplem2  6819  sbthlem2  6923  sbthlemi3  6924  djuss  7035  caseinl  7056  caseinr  7057  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  nqprrnd  7484  nqprxx  7487  ltexprlempr  7549  recexprlempr  7573  cauappcvgprlemcl  7594  caucvgprlemcl  7617  caucvgprprlemcl  7645  suplocsrlempr  7748  lemulge11  8761  nn0ge2m1nn  9174  frecfzennn  10361  reccn2ap  11254  demoivreALT  11714  pcdiv  12234  topcld  12749  metrest  13146  pwle2  13878