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  5523  respreima  5691  fpr  5745  dmtpos  6315  ixpsnf1o  6796  ssdomg  6838  exmidfodomrlemim  7270  archnqq  7486  recexgt0sr  7842  ige2m2fzo  10276  climeu  11463  algcvgblem  12227  qredeu  12275  qnumdencoprm  12371  qeqnumdivden  12372  eltg3i  14302  topbas  14313  neipsm  14400  lmbrf  14461  2lgslem1a  15339  exmidsbthrlem  15676