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  3202  unidif  3763  iunxdif2  3856  exss  4144  reg2exmidlema  4444  limom  4522  xpiindim  4671  relssres  4852  funco  5158  nfunsn  5448  fliftcnv  5689  fo1stresm  6052  fo2ndresm  6053  dftpos3  6152  tfri1d  6225  rdgtfr  6264  rdgruledefgg  6265  frectfr  6290  elixpsn  6622  mapxpen  6735  phplem2  6740  sbthlem2  6839  sbthlemi3  6840  djuss  6948  caseinl  6969  caseinr  6970  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  nqprrnd  7344  nqprxx  7347  ltexprlempr  7409  recexprlempr  7433  cauappcvgprlemcl  7454  caucvgprlemcl  7477  caucvgprprlemcl  7505  suplocsrlempr  7608  lemulge11  8617  nn0ge2m1nn  9030  frecfzennn  10192  reccn2ap  11075  demoivreALT  11469  topcld  12267  metrest  12664  pwle2  13182