MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jctild Structured version   Visualization version   GIF version

Theorem jctild 565
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
StepHypRef Expression
1 jctild.2 . . 3 (𝜑𝜃)
21a1d 25 . 2 (𝜑 → (𝜓𝜃))
3 jctild.1 . 2 (𝜑 → (𝜓𝜒))
42, 3jcad 555 1 (𝜑 → (𝜓 → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  syl6an  567  anc2li  579  ordunidif  5742  isofrlem  6555  dfwe2  6943  orduniorsuc  6992  poxp  7249  fnse  7254  ssenen  8094  dffi3  8297  fpwwe2lem13  9424  zmulcl  11386  rpneg  11823  rexuz3  14038  cau3lem  14044  climrlim2  14228  o1rlimmul  14299  iseralt  14365  gcdzeq  15214  isprm3  15339  vdwnnlem2  15643  ablfaclem3  18426  epttop  20753  lmcnp  21048  dfconn2  21162  txcnp  21363  cmphaushmeo  21543  isfild  21602  cnpflf2  21744  flimfnfcls  21772  alexsubALT  21795  fgcfil  23009  bcthlem5  23065  ivthlem2  23161  ivthlem3  23162  dvfsumrlim  23732  plypf1  23906  axeuclidlem  25776  usgr2wlkneq  26555  wwlksnredwwlkn0  26694  wwlksnextwrd  26695  wwlksnextproplem1  26707  clwlkclwwlklem2a1  26794  numclwwlkovf2ex  27109  extwwlkfab  27112  lnon0  27541  hstles  28978  mdsl1i  29068  atcveq0  29095  atcvat4i  29144  cdjreui  29179  issgon  30009  connpconn  30978  tfisg  31470  frmin  31493  outsideofrflx  31929  isbasisrelowllem1  32874  isbasisrelowllem2  32875  poimirlem3  33083  poimirlem29  33109  poimir  33113  heicant  33115  equivtotbnd  33248  ismtybndlem  33276  cvrat4  34248  linepsubN  34557  pmapsub  34573  osumcllem4N  34764  pexmidlem1N  34775  dochexmidlem1  36268  clcnvlem  37450  2reu1  40520  iccpartimp  40681  bgoldbwt  40990  bgoldbst  40991  elsetrecslem  41767
  Copyright terms: Public domain W3C validator