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  1806  funtp  5383  foimacnv  5601  respreima  5775  fpr  5835  dmtpos  6421  ixpsnf1o  6904  ssdomg  6951  exmidfodomrlemim  7411  archnqq  7636  recexgt0sr  7992  ige2m2fzo  10442  swrdlsw  11249  climeu  11856  algcvgblem  12620  qredeu  12668  qnumdencoprm  12764  qeqnumdivden  12765  eltg3i  14779  topbas  14790  neipsm  14877  lmbrf  14938  2lgslem1a  15816  usgredg2v  16074  exmidsbthrlem  16626