Theorem jctir 307

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 301	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  jctr  309  equvini  1695  funtp  5101  foimacnv  5306  respreima  5466  fpr  5518  dmtpos  6059  ixpsnf1o  6533  ssdomg  6575  exmidfodomrlemim  6924  archnqq  7073  recexgt0sr  7416  ige2m2fzo  9758  climeu  10855  algcvgblem  11474  qredeu  11522  qnumdencoprm  11614  qeqnumdivden  11615  eltg3i  11924  topbas  11935  neipsm  12022  lmbrf  12082  exmidsbthrlem  12633