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  1806  funtp  5383  foimacnv  5601  respreima  5775  fpr  5836  dmtpos  6422  ixpsnf1o  6905  ssdomg  6952  exmidfodomrlemim  7412  archnqq  7637  recexgt0sr  7993  ige2m2fzo  10444  swrdlsw  11254  climeu  11861  algcvgblem  12626  qredeu  12674  qnumdencoprm  12770  qeqnumdivden  12771  eltg3i  14786  topbas  14797  neipsm  14884  lmbrf  14945  2lgslem1a  15823  usgredg2v  16081  exmidsbthrlem  16652