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  3294  unidif  3871  iunxdif2  3965  exss  4260  reg2exmidlema  4570  limom  4650  xpiindim  4803  relssres  4984  funco  5298  nfunsn  5593  fliftcnv  5842  fo1stresm  6219  fo2ndresm  6220  dftpos3  6320  tfri1d  6393  rdgtfr  6432  rdgruledefgg  6433  frectfr  6458  elixpsn  6794  mapxpen  6909  phplem2  6914  sbthlem2  7024  sbthlemi3  7025  djuss  7136  caseinl  7157  caseinr  7158  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  2omotaplemap  7324  nqprrnd  7610  nqprxx  7613  ltexprlempr  7675  recexprlempr  7699  cauappcvgprlemcl  7720  caucvgprlemcl  7743  caucvgprprlemcl  7771  suplocsrlempr  7874  lemulge11  8893  nn0ge2m1nn  9309  frecfzennn  10518  wrdlenge2n0  10970  reccn2ap  11478  demoivreALT  11939  pcdiv  12471  idghm  13389  subrgid  13779  mulgghm2  14164  topcld  14345  metrest  14742  2lgs  15345  pwle2  15643