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  3336  unidif  3923  iunxdif2  4017  exss  4317  reg2exmidlema  4630  limom  4710  xpiindim  4865  relssres  5049  funco  5364  nfunsn  5672  fliftcnv  5931  fo1stresm  6319  fo2ndresm  6320  dftpos3  6423  tfri1d  6496  rdgtfr  6535  rdgruledefgg  6536  frectfr  6561  elixpsn  6899  mapxpen  7029  phplem2  7034  sbthlem2  7151  sbthlemi3  7152  djuss  7263  caseinl  7284  caseinr  7285  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  2omotaplemap  7469  nqprrnd  7756  nqprxx  7759  ltexprlempr  7821  recexprlempr  7845  cauappcvgprlemcl  7866  caucvgprlemcl  7889  caucvgprprlemcl  7917  suplocsrlempr  8020  lemulge11  9039  nn0ge2m1nn  9455  frecfzennn  10681  wrdlenge2n0  11142  swrdnd  11233  reccn2ap  11867  demoivreALT  12328  pcdiv  12868  idghm  13839  subrgid  14230  mulgghm2  14615  topcld  14826  metrest  15223  2lgs  15826  pwle2  16549