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  3335  unidif  3920  iunxdif2  4014  exss  4313  reg2exmidlema  4626  limom  4706  xpiindim  4859  relssres  5043  funco  5358  nfunsn  5666  fliftcnv  5925  fo1stresm  6313  fo2ndresm  6314  dftpos3  6414  tfri1d  6487  rdgtfr  6526  rdgruledefgg  6527  frectfr  6552  elixpsn  6890  mapxpen  7017  phplem2  7022  sbthlem2  7133  sbthlemi3  7134  djuss  7245  caseinl  7266  caseinr  7267  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  2omotaplemap  7451  nqprrnd  7738  nqprxx  7741  ltexprlempr  7803  recexprlempr  7827  cauappcvgprlemcl  7848  caucvgprlemcl  7871  caucvgprprlemcl  7899  suplocsrlempr  8002  lemulge11  9021  nn0ge2m1nn  9437  frecfzennn  10656  wrdlenge2n0  11115  swrdnd  11199  reccn2ap  11832  demoivreALT  12293  pcdiv  12833  idghm  13804  subrgid  14195  mulgghm2  14580  topcld  14791  metrest  15188  2lgs  15791  pwle2  16393