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  3340  unidif  3930  iunxdif2  4024  exss  4325  reg2exmidlema  4638  limom  4718  xpiindim  4873  relssres  5057  funco  5373  nfunsn  5685  fliftcnv  5946  fo1stresm  6333  fo2ndresm  6334  dftpos3  6471  tfri1d  6544  rdgtfr  6583  rdgruledefgg  6584  frectfr  6609  elixpsn  6947  mapxpen  7077  phplem2  7082  sbthlem2  7200  sbthlemi3  7201  djuss  7312  caseinl  7333  caseinr  7334  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  2omotaplemap  7519  nqprrnd  7806  nqprxx  7809  ltexprlempr  7871  recexprlempr  7895  cauappcvgprlemcl  7916  caucvgprlemcl  7939  caucvgprprlemcl  7967  suplocsrlempr  8070  lemulge11  9089  nn0ge2m1nn  9505  frecfzennn  10732  wrdlenge2n0  11196  swrdnd  11287  reccn2ap  11934  demoivreALT  12396  pcdiv  12936  idghm  13907  subrgid  14299  mulgghm2  14684  topcld  14900  metrest  15297  2lgs  15903  pwle2  16700