Theorem jctild 543

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

Hypotheses

Ref	Expression
jctild.1
jctild.2

Assertion

Ref	Expression
jctild

Proof of Theorem jctild

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

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  syl6an  545  anc2li  557  ifpfal  1389  2eu1OLD  2377  reusv7OLD  4664  ordunidif  4931  isofrlem  6236  dfwe2  6617  orduniorsuc  6665  poxp  6912  fnse  6917  ssenen  7711  dffi3  7911  fpwwe2lem13  9041  zmulcl  10937  rpneg  11278  rexuz3  13181  cau3lem  13187  climrlim2  13370  o1rlimmul  13441  iseralt  13507  gcdeq  14190  isprm3  14226  vdwnnlem2  14514  ablfaclem3  17138  epttop  19510  lmcnp  19805  dfcon2  19920  txcnp  20121  cmphaushmeo  20301  isfild  20359  cnpflf2  20501  flimfnfcls  20529  alexsubALT  20551  fgcfil  21710  bcthlem5  21767  ivthlem2  21864  ivthlem3  21865  dvfsumrlim  22432  plypf1  22609  axeuclidlem  24265  wwlknredwwlkn0  24727  wwlkextwrd  24728  wwlkextproplem1  24741  clwlkisclwwlklem2a1  24779  rusgranumwlklem1  24949  numclwwlkovf2ex  25086  extwwlkfab  25090  lnon0  25713  hstles  27150  mdsl1i  27240  atcveq0  27267  atcvat4i  27316  cdjreui  27351  issgon  28123  conpcon  28680  tfisg  29284  frmin  29322  outsideofrflx  29777  heicant  30049  equivtotbnd  30274  ismtybndlem  30302  2reu1  32191  cvrat4  35167  linepsubN  35476  pmapsub  35492  osumcllem4N  35683  pexmidlem1N  35694  dochexmidlem1  37187

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