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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  jctl  314  ddifnel  3360  unidif  3967  iunxdif2  4061  exss  4367  reg2exmidlema  4681  limom  4761  xpiindim  4917  relssres  5101  funco  5417  nfunsn  5733  fliftcnv  6001  fo1stresm  6395  fo2ndresm  6396  dftpos3  6533  tfri1d  6606  rdgtfr  6645  rdgruledefgg  6646  frectfr  6671  elixpsn  7017  mapxpen  7148  phplem2  7154  sbthlem2  7275  sbthlemi3  7276  djuss  7411  caseinl  7432  caseinr  7433  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  2omotaplemap  7624  nqprrnd  7911  nqprxx  7914  ltexprlempr  7976  recexprlempr  8000  cauappcvgprlemcl  8021  caucvgprlemcl  8044  caucvgprprlemcl  8072  suplocsrlempr  8175  lemulge11  9199  nn0ge2m1nn  9632  frecfzennn  10877  hashfibclem  11297  wrdlenge2n0  11355  swrdnd  11446  reccn2ap  12097  demoivreALT  12559  pcdiv  13103  ballotfilemfc0  13283  ballotfilemfcc  13284  idghm  14113  subrgid  14582  mulgghm2  14994  topcld  15262  metrest  15659  2lgs  16345  pwle2  17150