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  3338  unidif  3925  iunxdif2  4019  exss  4319  reg2exmidlema  4632  limom  4712  xpiindim  4867  relssres  5051  funco  5366  nfunsn  5676  fliftcnv  5936  fo1stresm  6324  fo2ndresm  6325  dftpos3  6428  tfri1d  6501  rdgtfr  6540  rdgruledefgg  6541  frectfr  6566  elixpsn  6904  mapxpen  7034  phplem2  7039  sbthlem2  7157  sbthlemi3  7158  djuss  7269  caseinl  7290  caseinr  7291  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  2omotaplemap  7476  nqprrnd  7763  nqprxx  7766  ltexprlempr  7828  recexprlempr  7852  cauappcvgprlemcl  7873  caucvgprlemcl  7896  caucvgprprlemcl  7924  suplocsrlempr  8027  lemulge11  9046  nn0ge2m1nn  9462  frecfzennn  10689  wrdlenge2n0  11153  swrdnd  11244  reccn2ap  11878  demoivreALT  12340  pcdiv  12880  idghm  13851  subrgid  14243  mulgghm2  14628  topcld  14839  metrest  15236  2lgs  15839  pwle2  16625