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  1768  funtp  5281  foimacnv  5491  respreima  5657  fpr  5711  dmtpos  6270  ixpsnf1o  6749  ssdomg  6791  exmidfodomrlemim  7213  archnqq  7429  recexgt0sr  7785  ige2m2fzo  10211  climeu  11317  algcvgblem  12062  qredeu  12110  qnumdencoprm  12206  qeqnumdivden  12207  eltg3i  13827  topbas  13838  neipsm  13925  lmbrf  13986  exmidsbthrlem  15042