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  1804  funtp  5374  foimacnv  5592  respreima  5765  fpr  5825  dmtpos  6408  ixpsnf1o  6891  ssdomg  6938  exmidfodomrlemim  7390  archnqq  7615  recexgt0sr  7971  ige2m2fzo  10416  swrdlsw  11216  climeu  11822  algcvgblem  12586  qredeu  12634  qnumdencoprm  12730  qeqnumdivden  12731  eltg3i  14745  topbas  14756  neipsm  14843  lmbrf  14904  2lgslem1a  15782  usgredg2v  16037  exmidsbthrlem  16450