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  1804  funtp  5380  foimacnv  5598  respreima  5771  fpr  5831  dmtpos  6417  ixpsnf1o  6900  ssdomg  6947  exmidfodomrlemim  7402  archnqq  7627  recexgt0sr  7983  ige2m2fzo  10433  swrdlsw  11240  climeu  11847  algcvgblem  12611  qredeu  12659  qnumdencoprm  12755  qeqnumdivden  12756  eltg3i  14770  topbas  14781  neipsm  14868  lmbrf  14929  2lgslem1a  15807  usgredg2v  16063  exmidsbthrlem  16562