Theorem jctil 310

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 304	1 ⊢ (𝜑 → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  jctl  312  ddifnel  3248  unidif  3815  iunxdif2  3908  exss  4199  reg2exmidlema  4505  limom  4585  xpiindim  4735  relssres  4916  funco  5222  nfunsn  5514  fliftcnv  5757  fo1stresm  6121  fo2ndresm  6122  dftpos3  6221  tfri1d  6294  rdgtfr  6333  rdgruledefgg  6334  frectfr  6359  elixpsn  6692  mapxpen  6805  phplem2  6810  sbthlem2  6914  sbthlemi3  6915  djuss  7026  caseinl  7047  caseinr  7048  exmidfodomrlemr  7149  exmidfodomrlemrALT  7150  nqprrnd  7475  nqprxx  7478  ltexprlempr  7540  recexprlempr  7564  cauappcvgprlemcl  7585  caucvgprlemcl  7608  caucvgprprlemcl  7636  suplocsrlempr  7739  lemulge11  8752  nn0ge2m1nn  9165  frecfzennn  10351  reccn2ap  11240  demoivreALT  11700  pcdiv  12211  topcld  12650  metrest  13047  pwle2  13712