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  3360  unidif  3965  iunxdif2  4059  exss  4365  reg2exmidlema  4679  limom  4759  xpiindim  4915  relssres  5099  funco  5415  nfunsn  5730  fliftcnv  5995  fo1stresm  6389  fo2ndresm  6390  dftpos3  6527  tfri1d  6600  rdgtfr  6639  rdgruledefgg  6640  frectfr  6665  elixpsn  7011  mapxpen  7142  phplem2  7148  sbthlem2  7269  sbthlemi3  7270  djuss  7404  caseinl  7425  caseinr  7426  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  2omotaplemap  7617  nqprrnd  7904  nqprxx  7907  ltexprlempr  7969  recexprlempr  7993  cauappcvgprlemcl  8014  caucvgprlemcl  8037  caucvgprprlemcl  8065  suplocsrlempr  8168  lemulge11  9190  nn0ge2m1nn  9610  frecfzennn  10846  hashfibclem  11265  wrdlenge2n0  11323  swrdnd  11414  reccn2ap  12062  demoivreALT  12524  pcdiv  13064  ballotfilemfc0  13215  ballotfilemfcc  13216  idghm  14045  subrgid  14514  mulgghm2  14926  topcld  15193  metrest  15590  2lgs  16206  pwle2  17011