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  3349  unidif  3945  iunxdif2  4039  exss  4342  reg2exmidlema  4655  limom  4735  xpiindim  4891  relssres  5075  funco  5391  nfunsn  5706  fliftcnv  5967  fo1stresm  6354  fo2ndresm  6355  dftpos3  6492  tfri1d  6565  rdgtfr  6604  rdgruledefgg  6605  frectfr  6630  elixpsn  6969  mapxpen  7100  phplem2  7106  sbthlem2  7227  sbthlemi3  7228  djuss  7360  caseinl  7381  caseinr  7382  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  2omotaplemap  7570  nqprrnd  7857  nqprxx  7860  ltexprlempr  7922  recexprlempr  7946  cauappcvgprlemcl  7967  caucvgprlemcl  7990  caucvgprprlemcl  8018  suplocsrlempr  8121  lemulge11  9139  nn0ge2m1nn  9559  frecfzennn  10787  hashfibclem  11202  wrdlenge2n0  11256  swrdnd  11347  reccn2ap  11994  demoivreALT  12456  pcdiv  12996  idghm  13968  subrgid  14360  mulgghm2  14748  topcld  14966  metrest  15363  2lgs  15969  pwle2  16764