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  3278  unidif  3853  iunxdif2  3947  exss  4239  reg2exmidlema  4545  limom  4625  xpiindim  4776  relssres  4957  funco  5268  nfunsn  5561  fliftcnv  5809  fo1stresm  6175  fo2ndresm  6176  dftpos3  6276  tfri1d  6349  rdgtfr  6388  rdgruledefgg  6389  frectfr  6414  elixpsn  6748  mapxpen  6861  phplem2  6866  sbthlem2  6970  sbthlemi3  6971  djuss  7082  caseinl  7103  caseinr  7104  exmidfodomrlemr  7214  exmidfodomrlemrALT  7215  2omotaplemap  7269  nqprrnd  7555  nqprxx  7558  ltexprlempr  7620  recexprlempr  7644  cauappcvgprlemcl  7665  caucvgprlemcl  7688  caucvgprprlemcl  7716  suplocsrlempr  7819  lemulge11  8836  nn0ge2m1nn  9249  frecfzennn  10439  reccn2ap  11334  demoivreALT  11794  pcdiv  12315  subrgid  13438  topcld  13880  metrest  14277  pwle2  15020