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  1782  funtp  5341  foimacnv  5557  respreima  5726  fpr  5784  dmtpos  6360  ixpsnf1o  6841  ssdomg  6888  exmidfodomrlemim  7335  archnqq  7560  recexgt0sr  7916  ige2m2fzo  10359  swrdlsw  11155  climeu  11692  algcvgblem  12456  qredeu  12504  qnumdencoprm  12600  qeqnumdivden  12601  eltg3i  14613  topbas  14624  neipsm  14711  lmbrf  14772  2lgslem1a  15650  exmidsbthrlem  16133