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  3335  unidif  3920  iunxdif2  4014  exss  4314  reg2exmidlema  4627  limom  4707  xpiindim  4862  relssres  5046  funco  5361  nfunsn  5669  fliftcnv  5928  fo1stresm  6316  fo2ndresm  6317  dftpos3  6419  tfri1d  6492  rdgtfr  6531  rdgruledefgg  6532  frectfr  6557  elixpsn  6895  mapxpen  7022  phplem2  7027  sbthlem2  7141  sbthlemi3  7142  djuss  7253  caseinl  7274  caseinr  7275  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  2omotaplemap  7459  nqprrnd  7746  nqprxx  7749  ltexprlempr  7811  recexprlempr  7835  cauappcvgprlemcl  7856  caucvgprlemcl  7879  caucvgprprlemcl  7907  suplocsrlempr  8010  lemulge11  9029  nn0ge2m1nn  9445  frecfzennn  10665  wrdlenge2n0  11125  swrdnd  11212  reccn2ap  11845  demoivreALT  12306  pcdiv  12846  idghm  13817  subrgid  14208  mulgghm2  14593  topcld  14804  metrest  15201  2lgs  15804  pwle2  16477