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  1807  funtp  5409  foimacnv  5632  respreima  5805  fpr  5866  dmtpos  6487  ixpsnf1o  6971  ssdomg  7018  exmidfodomrlemim  7504  archnqq  7732  recexgt0sr  8088  ige2m2fzo  10543  swrdlsw  11361  climeu  11981  algcvgblem  12746  qredeu  12794  qnumdencoprm  12890  qeqnumdivden  12891  eltg3i  14921  topbas  14932  neipsm  15019  lmbrf  15080  2lgslem1a  15961  usgredg2v  16219  exmidsbthrlem  16802