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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  jctr  315  equvini  1811  funtp  5434  foimacnv  5657  respreima  5836  fpr  5897  dmtpos  6527  ixpsnf1o  7018  ssdomg  7065  exmidfodomrlemim  7554  archnqq  7785  recexgt0sr  8141  ige2m2fzo  10627  swrdlsw  11457  climeu  12081  algcvgblem  12846  qredeu  12894  qnumdencoprm  12992  qeqnumdivden  12993  ballotfilemfc0  13284  ballotfilemfcc  13285  eltg3i  15248  topbas  15259  neipsm  15346  lmbrf  15407  bcmono  16265  2lgslem1a  16373  usgredg2v  16631  exmidsbthrlem  17233