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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  jctl  314  ddifnel  3360  unidif  3967  iunxdif2  4061  exss  4369  reg2exmidlema  4683  limom  4763  xpiindim  4919  relssres  5103  funco  5420  nfunsn  5736  fliftcnv  6004  fo1stresm  6399  fo2ndresm  6400  dftpos3  6538  tfri1d  6611  rdgtfr  6650  rdgruledefgg  6651  frectfr  6676  elixpsn  7023  mapxpen  7154  phplem2  7160  sbthlem2  7282  sbthlemi3  7283  djuss  7417  caseinl  7438  caseinr  7439  exmidfodomrlemr  7561  exmidfodomrlemrALT  7562  2omotaplemap  7630  nqprrnd  7917  nqprxx  7920  ltexprlempr  7982  recexprlempr  8006  cauappcvgprlemcl  8027  caucvgprlemcl  8050  caucvgprprlemcl  8078  suplocsrlempr  8181  lemulge11  9205  nn0ge2m1nn  9637  frecfzennn  10884  hashfibclem  11304  wrdlenge2n0  11362  swrdnd  11453  reccn2ap  12104  demoivreALT  12566  pcdiv  13110  ballotfilemfc0  13290  ballotfilemfcc  13291  idghm  14121  subrgid  14640  mulgghm2  15052  psrbagmax  15190  topcld  15368  metrest  15765  2lgs  16461  pwle2  17266