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  11578  algcvgblem  12342  qredeu  12390  qnumdencoprm  12486  qeqnumdivden  12487  eltg3i  14499  topbas  14510  neipsm  14597  lmbrf  14658  2lgslem1a  15536  exmidsbthrlem  15923