Theorem jctird 544

Description: Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.)

Hypotheses

Ref	Expression
jctird.1
jctird.2

Assertion

Ref	Expression
jctird

Proof of Theorem jctird

Step	Hyp	Ref	Expression
1		jctird.1	. 2
2		jctird.2	. . 3
3	2	a1d 25	. 2
4	1, 3	jcad 533	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  anc2ri  558  ifptru  1388  fnun  5692  fco  5746  mapdom2  7708  fisupg  7788  fiint  7817  dffi3  7911  dfac2  8532  cflm  8651  cfslbn  8668  cardmin  8960  fpwwe2lem12  9040  fpwwe2lem13  9041  elfznelfzob  11916  isprm5  14253  latjlej1  15695  latmlem1  15711  cnrest2  19787  cnpresti  19789  trufil  20411  stdbdxmet  21018  lgsdir  23605  usgraedg4  24387  wlkdvspth  24610  el2spthonot  24870  orthin  26364  mdbr2  27215  dmdbr2  27222  mdsl2i  27241  atcvat4i  27316  mdsymlem3  27324  wzel  29380  ontgval  29896  cmtbr4N  34980  cvrat4  35167  cdlemblem  35517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371