MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jctl Structured version   Unicode version

Theorem jctl 541
Description: Inference conjoining a theorem to the left of a consequent. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.)
Hypothesis
Ref Expression
jctl.1  |-  ps
Assertion
Ref Expression
jctl  |-  ( ph  ->  ( ps  /\  ph ) )

Proof of Theorem jctl
StepHypRef Expression
1 id 22 . 2  |-  ( ph  ->  ph )
2 jctl.1 . 2  |-  ps
31, 2jctil 537 1  |-  ( ph  ->  ( ps  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  mpanl1  680  mpanlr1  686  relop  5151  odi  7225  cdaun  8548  nn0n0n1ge2  10855  0mod  11991  expge1  12167  hashge2el2dif  12483  swrd2lsw  12849  ndvdsp1  13922  istrkg2ld  23586  cusgra3vnbpr  24141  constr2spthlem1  24272  2pthon  24280  constr3trllem2  24327  constr3pthlem1  24331  constr3pthlem2  24332  wlkiswwlk2  24373  ococin  26002  cmbr4i  26195  iundifdif  27103  nepss  28570  axextndbi  28814  ontopbas  29470  mblfinlem4  29631  ismblfin  29632  fiphp3d  30357  eelT01  32583  eel0T1  32584  un01  32666  bj-elccinfty  33689
  Copyright terms: Public domain W3C validator