HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem jctir 293
Description: Inference conjoining a theorem to right of consequent in an implication.
Hypotheses
Ref Expression
jctir.1 |- (ph -> ps)
jctir.2 |- ch
Assertion
Ref Expression
jctir |- (ph -> (ps /\ ch))
Proof of Theorem jctir
StepHypRef Expression
1 jctir.1 . 2 |- (ph -> ps)
2 jctir.2 . . 3 |- ch
32a1i 8 . 2 |- (ph -> ch)
41, 3jca 288 1 |- (ph -> (ps /\ ch))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223
This theorem is referenced by:  equvini 1164  csbiegf 2021  intmin 2543  intab 2550  ordsseleq 2966  ordunidif 2995  onssmin 2998  fn0 3591  fnopabfv 3743  fsn 3819  tfrlem10 3905  tz7.44-3 3915  curry1 4082  oawordeulem 4172  oelim2 4206  ixp0 4345  ssdomg 4389  fodomr 4463  limenpsi 4485  phplem4 4491  php 4493  ominf 4508  pssnn 4513  fodomfi 4540  suppr 4562  supsnALT 4564  aceq3lem 4704  aceq6b 4714  cfsuc 4887  prlem934a 5109  reclem2pr 5129  recexsrlem 5184  map2psrpr 5192  supsrlem2 5198  ltsor 5233  posex 5856  nnsub 5903  sqr0 6602  creur 6673  creui 6674  bcxmas 7014  climeu 7037  fnsmntlem 7160  fnsmnt 7161  efaddlem10 7289  efaddlem17 7296  efaddlem23 7302  acdc2lem2 7431  acdc5lem2 7434  ruclem33 7485  ruclem35 7487  infxpidmlem7 7501  infunabs 7508  infcdaabs 7509  alephexp2 7528  topbast 7569  neips 7668  blelrn 7788  grpfo 7977  nvex 8169  nmcnc 8276  nmosetn0 8360  normgt0tOLD 8914  normgt0t 8915  hhsst 9056  occllem4 9092  occllem6 9094  projlem8 9109  projlem13 9114  projlem15 9116  projlem24 9125  projlem25 9126  projlem26 9127  projlem29 9130  pjthlem4 9137  pjthlem7 9140  pjthlem10 9143  pjthlem11 9144  pjthlem12 9145  pjoc1 9179  shlej1 9263  chlejb1 9314  cmbr4 9461  pjjs 9562  adjvalvalt 9777  nmopunt 9854  pjnormss 10007  stge1 10075  stle0 10076  stles 10078  stadd 10083  stadd3 10085  mdsl2b 10158  mdslmd1lem1 10160  faimpex 10339  cdrci 10381  truni1 10386  fgsb 10444  efilcp 10445  fgsb2 10449  cnfilca 10451  dtopcl 10459  dmse1 10467  mslb1 10473  msra3 10475  iintlem1 10476
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 147  df-an 225
Copyright terms: Public domain