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	|- ( ph -> ps )
jctil.2	|- ch

Assertion

Ref	Expression
jctir	|- ( ph -> ( ps /\ ch ) )

Proof of Theorem jctir

Step	Hyp	Ref	Expression
1		jctil.1	. 2 |- ( ph -> ps )
2		jctil.2	. . 3 |- ch
3	2	a1i 9	. 2 |- ( ph -> ch )
4	1, 3	jca 306	1 |- ( ph -> ( ps /\ ch ) )

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  5437  foimacnv  5660  respreima  5839  fpr  5900  dmtpos  6531  ixpsnf1o  7022  ssdomg  7069  exmidfodomrlemim  7559  archnqq  7790  recexgt0sr  8146  ige2m2fzo  10633  swrdlsw  11463  climeu  12087  algcvgblem  12852  qredeu  12900  qnumdencoprm  12998  qeqnumdivden  12999  ballotfilemfc0  13290  ballotfilemfcc  13291  eltg3i  15282  topbas  15293  neipsm  15380  lmbrf  15441  bcmono  16304  2lgslem1a  16412  usgredg2v  16670  exmidsbthrlem  17273