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  1732  funtp  5184  foimacnv  5393  respreima  5556  fpr  5610  dmtpos  6161  ixpsnf1o  6638  ssdomg  6680  exmidfodomrlemim  7074  archnqq  7249  recexgt0sr  7605  ige2m2fzo  10006  climeu  11097  algcvgblem  11766  qredeu  11814  qnumdencoprm  11907  qeqnumdivden  11908  eltg3i  12264  topbas  12275  neipsm  12362  lmbrf  12423  exmidsbthrlem  13392