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  1780  funtp  5326  foimacnv  5539  respreima  5707  fpr  5765  dmtpos  6341  ixpsnf1o  6822  ssdomg  6869  exmidfodomrlemim  7308  archnqq  7529  recexgt0sr  7885  ige2m2fzo  10325  climeu  11549  algcvgblem  12313  qredeu  12361  qnumdencoprm  12457  qeqnumdivden  12458  eltg3i  14470  topbas  14481  neipsm  14568  lmbrf  14629  2lgslem1a  15507  exmidsbthrlem  15894