Theorem jctir 311

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  jctr  313  equvini  1751  funtp  5249  foimacnv  5458  respreima  5622  fpr  5676  dmtpos  6233  ixpsnf1o  6711  ssdomg  6753  exmidfodomrlemim  7167  archnqq  7368  recexgt0sr  7724  ige2m2fzo  10143  climeu  11248  algcvgblem  11992  qredeu  12040  qnumdencoprm  12136  qeqnumdivden  12137  eltg3i  12811  topbas  12822  neipsm  12909  lmbrf  12970  exmidsbthrlem  14016