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  3306  unidif  3885  iunxdif2  3979  exss  4276  reg2exmidlema  4587  limom  4667  xpiindim  4820  relssres  5003  funco  5317  nfunsn  5621  fliftcnv  5874  fo1stresm  6257  fo2ndresm  6258  dftpos3  6358  tfri1d  6431  rdgtfr  6470  rdgruledefgg  6471  frectfr  6496  elixpsn  6832  mapxpen  6957  phplem2  6962  sbthlem2  7072  sbthlemi3  7073  djuss  7184  caseinl  7205  caseinr  7206  exmidfodomrlemr  7323  exmidfodomrlemrALT  7324  2omotaplemap  7382  nqprrnd  7669  nqprxx  7672  ltexprlempr  7734  recexprlempr  7758  cauappcvgprlemcl  7779  caucvgprlemcl  7802  caucvgprprlemcl  7830  suplocsrlempr  7933  lemulge11  8952  nn0ge2m1nn  9368  frecfzennn  10584  wrdlenge2n0  11042  swrdnd  11126  reccn2ap  11674  demoivreALT  12135  pcdiv  12675  idghm  13645  subrgid  14035  mulgghm2  14420  topcld  14631  metrest  15028  2lgs  15631  pwle2  16050