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  5411  foimacnv  5634  respreima  5807  fpr  5868  dmtpos  6489  ixpsnf1o  6973  ssdomg  7020  exmidfodomrlemim  7506  archnqq  7734  recexgt0sr  8090  ige2m2fzo  10547  swrdlsw  11365  climeu  11985  algcvgblem  12750  qredeu  12798  qnumdencoprm  12894  qeqnumdivden  12895  ballotfilemfc0  13153  ballotfilemfcc  13154  eltg3i  14938  topbas  14949  neipsm  15036  lmbrf  15097  2lgslem1a  15978  usgredg2v  16236  exmidsbthrlem  16819