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  5390  foimacnv  5610  respreima  5783  fpr  5844  dmtpos  6465  ixpsnf1o  6948  ssdomg  6995  exmidfodomrlemim  7455  archnqq  7680  recexgt0sr  8036  ige2m2fzo  10489  swrdlsw  11299  climeu  11919  algcvgblem  12684  qredeu  12732  qnumdencoprm  12828  qeqnumdivden  12829  eltg3i  14850  topbas  14861  neipsm  14948  lmbrf  15009  2lgslem1a  15890  usgredg2v  16148  exmidsbthrlem  16733