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  1769  funtp  5308  foimacnv  5519  respreima  5687  fpr  5741  dmtpos  6311  ixpsnf1o  6792  ssdomg  6834  exmidfodomrlemim  7263  archnqq  7479  recexgt0sr  7835  ige2m2fzo  10268  climeu  11442  algcvgblem  12190  qredeu  12238  qnumdencoprm  12334  qeqnumdivden  12335  eltg3i  14235  topbas  14246  neipsm  14333  lmbrf  14394  2lgslem1a  15245  exmidsbthrlem  15582