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

Step	Hyp	Ref	Expression
1		jctir.1	. 2 |- (ph -> ps)
2		jctir.2	. . 3 |- ch
3	2	a1i 8	. 2 |- (ph -> ch)
4	1, 3	jca 288	1 |- (ph -> (ps /\ ch))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  equvini 1168  csbiegf 2031  intmin 2553  intab 2560  ordsseleq 2976  ordunidif 3005  onssmin 3008  fn0 3605  fnopabfv 3758  fsn 3834  tfrlem10 3920  tz7.44-3 3930  curry1 4098  oawordeulem 4188  oelim2 4222  ixp0 4361  ssdomg 4407  fodomr 4481  limenpsi 4503  phplem4 4509  php 4511  ominf 4526  pssnn 4531  fodomfi 4558  suppr 4582  supsnALT 4584  aceq3lem 4724  aceq6b 4734  cfsuc 4907  prlem934a 5129  reclem2pr 5149  recexsrlem 5204  map2psrpr 5212  supsrlem2 5218  ltsor 5253  posex 5896  nnsub 5944  sqr0 6658  creur 6728  creui 6729  bcxmas 7061  climeu 7085  fnsmntlem 7210  fnsmnt 7211  efaddlem10 7332  efaddlem17 7339  efaddlem23 7345  acdc2lem2 7474  acdc5lem2 7477  ruclem33 7527  ruclem35 7529  infxpidmlem7 7543  infunabs 7550  infcdaabs 7551  alephexp2 7571  topbast 7612  neips 7712  blelrn 7833  grpfo 8028  nvex 8215  nmcn3 8326  nmcnc 8327  nmosetn0 8413  spwpr3OLD 8647  normgt0tOLD 8978  normgt0t 8979  hhsst 9121  occllem4 9161  occllem6 9163  projlem8 9178  projlem13 9183  projlem15 9185  projlem24 9194  projlem25 9195  projlem26 9196  projlem29 9199  pjthlem4 9207  pjthlem7 9210  pjthlem10 9213  pjthlem11 9214  pjthlem12 9215  pjoc1 9249  shlej1 9333  chlejb1 9384  cmbr4 9529  pjjs 9630  adjvalvalt 9846  nmopunt 9924  pjnormss 10081  stge1 10150  stle0 10151  stles 10153  stadd 10158  stadd3 10160  mdsl2b 10235  mdslmd1lem1 10237  faimpex 10422  cdrci 10466  truni1 10471  fgsb 10529  efilcp 10530  fgsb2 10535  cnfilca 10537  dtopcl 10558  dmse1 10566  mslb1 10572  msra3 10574  iintlem1 10575

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