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  5373  foimacnv  5589  respreima  5762  fpr  5820  dmtpos  6400  ixpsnf1o  6881  ssdomg  6928  exmidfodomrlemim  7375  archnqq  7600  recexgt0sr  7956  ige2m2fzo  10399  swrdlsw  11196  climeu  11802  algcvgblem  12566  qredeu  12614  qnumdencoprm  12710  qeqnumdivden  12711  eltg3i  14724  topbas  14735  neipsm  14822  lmbrf  14883  2lgslem1a  15761  usgredg2v  16016  exmidsbthrlem  16349