Theorem jctir 313

Description: Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.)

Hypotheses

Ref	Expression
jctil.1	⊢ (𝜑 → 𝜓)
jctil.2	⊢ 𝜒

Assertion

Ref	Expression
jctir	⊢ (𝜑 → (𝜓 ∧ 𝜒))

Proof of Theorem jctir

Step	Hyp	Ref	Expression
1		jctil.1	. 2 ⊢ (𝜑 → 𝜓)
2		jctil.2	. . 3 ⊢ 𝜒
3	2	a1i 9	. 2 ⊢ (𝜑 → 𝜒)
4	1, 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:  jctr  315  equvini  1772  funtp  5312  foimacnv  5525  respreima  5693  fpr  5747  dmtpos  6323  ixpsnf1o  6804  ssdomg  6846  exmidfodomrlemim  7282  archnqq  7503  recexgt0sr  7859  ige2m2fzo  10293  climeu  11480  algcvgblem  12244  qredeu  12292  qnumdencoprm  12388  qeqnumdivden  12389  eltg3i  14400  topbas  14411  neipsm  14498  lmbrf  14559  2lgslem1a  15437  exmidsbthrlem  15779