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  3258  unidif  3826  iunxdif2  3919  exss  4210  reg2exmidlema  4516  limom  4596  xpiindim  4746  relssres  4927  funco  5236  nfunsn  5528  fliftcnv  5772  fo1stresm  6138  fo2ndresm  6139  dftpos3  6239  tfri1d  6312  rdgtfr  6351  rdgruledefgg  6352  frectfr  6377  elixpsn  6711  mapxpen  6824  phplem2  6829  sbthlem2  6933  sbthlemi3  6934  djuss  7045  caseinl  7066  caseinr  7067  exmidfodomrlemr  7172  exmidfodomrlemrALT  7173  nqprrnd  7498  nqprxx  7501  ltexprlempr  7563  recexprlempr  7587  cauappcvgprlemcl  7608  caucvgprlemcl  7631  caucvgprprlemcl  7659  suplocsrlempr  7762  lemulge11  8775  nn0ge2m1nn  9188  frecfzennn  10375  reccn2ap  11269  demoivreALT  11729  pcdiv  12249  topcld  12868  metrest  13265  pwle2  13996