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  3335  unidif  3919  iunxdif2  4013  exss  4312  reg2exmidlema  4623  limom  4703  xpiindim  4856  relssres  5039  funco  5354  nfunsn  5658  fliftcnv  5912  fo1stresm  6297  fo2ndresm  6298  dftpos3  6398  tfri1d  6471  rdgtfr  6510  rdgruledefgg  6511  frectfr  6536  elixpsn  6872  mapxpen  6997  phplem2  7002  sbthlem2  7113  sbthlemi3  7114  djuss  7225  caseinl  7246  caseinr  7247  exmidfodomrlemr  7368  exmidfodomrlemrALT  7369  2omotaplemap  7431  nqprrnd  7718  nqprxx  7721  ltexprlempr  7783  recexprlempr  7807  cauappcvgprlemcl  7828  caucvgprlemcl  7851  caucvgprprlemcl  7879  suplocsrlempr  7982  lemulge11  9001  nn0ge2m1nn  9417  frecfzennn  10635  wrdlenge2n0  11093  swrdnd  11177  reccn2ap  11810  demoivreALT  12271  pcdiv  12811  idghm  13782  subrgid  14172  mulgghm2  14557  topcld  14768  metrest  15165  2lgs  15768  pwle2  16295