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 ) )

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  1811  funtp  5429  foimacnv  5652  respreima  5827  fpr  5888  dmtpos  6517  ixpsnf1o  7008  ssdomg  7055  exmidfodomrlemim  7543  archnqq  7774  recexgt0sr  8130  ige2m2fzo  10594  swrdlsw  11419  climeu  12040  algcvgblem  12805  qredeu  12853  qnumdencoprm  12949  qeqnumdivden  12950  ballotfilemfc0  13210  ballotfilemfcc  13211  eltg3i  15080  topbas  15091  neipsm  15178  lmbrf  15239  2lgslem1a  16121  usgredg2v  16379  exmidsbthrlem  16972