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  4369  reg2exmidlema  4683  limom  4763  xpiindim  4919  relssres  5103  funco  5420  nfunsn  5736  fliftcnv  6004  fo1stresm  6399  fo2ndresm  6400  dftpos3  6537  tfri1d  6610  rdgtfr  6649  rdgruledefgg  6650  frectfr  6675  elixpsn  7022  mapxpen  7153  phplem2  7159  sbthlem2  7281  sbthlemi3  7282  djuss  7417  caseinl  7438  caseinr  7439  exmidfodomrlemr  7561  exmidfodomrlemrALT  7562  2omotaplemap  7630  nqprrnd  7917  nqprxx  7920  ltexprlempr  7982  recexprlempr  8006  cauappcvgprlemcl  8027  caucvgprlemcl  8050  caucvgprprlemcl  8078  suplocsrlempr  8181  lemulge11  9205  nn0ge2m1nn  9639  frecfzennn  10885  hashfibclem  11305  wrdlenge2n0  11363  swrdnd  11454  reccn2ap  12105  demoivreALT  12567  pcdiv  13111  ballotfilemfc0  13291  ballotfilemfcc  13292  idghm  14122  subrgid  14641  mulgghm2  15053  topcld  15347  metrest  15744  2lgs  16440  pwle2  17245