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  6532  ixpsnf1o  7024  ssdomg  7071  exmidfodomrlemim  7559  archnqq  7790  recexgt0sr  8146  ige2m2fzo  10632  swrdlsw  11462  climeu  12086  algcvgblem  12851  qredeu  12899  qnumdencoprm  12997  qeqnumdivden  12998  ballotfilemfc0  13289  ballotfilemfcc  13290  eltg3i  15299  topbas  15310  neipsm  15397  lmbrf  15458  bcmono  16321  2lgslem1a  16429  usgredg2v  16687  exmidsbthrlem  17290