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 1170  csbiegf 2034  intmin 2557  intab 2564  ordsseleq 2982  ordunidif 3011  onssmin 3014  fn0 3611  fnopabfv 3764  fsn 3840  tfrlem10 3926  tz7.44-3 3936  curry1 4104  oawordeulem 4194  oelim2 4228  ixp0 4367  ssdomg 4414  fodomr 4489  limenpsi 4511  phplem4 4517  php 4519  ominf 4536  ominfOLD 4537  pssnn 4544  fodomfi 4575  fodomfiOLD 4576  suppr 4599  supsnALT 4601  aceq3lem 4742  aceq6b 4752  cfsuc 4927  prlem934a 5149  reclem2pr 5169  recexsrlem 5224  map2psrpr 5232  supsrlem2 5238  ltsor 5273  posex 5910  nnsub 5958  sqr0 6673  creur 6743  creui 6744  bcxmas 7076  climeu 7100  fnsmntlem 7225  fnsmnt 7226  efaddlem10 7347  efaddlem17 7354  efaddlem23 7360  acdc2lem2 7490  acdc5lem2 7493  ruclem33 7543  ruclem35 7545  infxpidmlem7 7559  infunabs 7566  infcdaabs 7567  alephexp2 7588  topbast 7626  neips 7724  blelrn 7845  grpfo 8040  nvex 8226  nmcn3 8337  nmcnc 8338  nmosetn0 8424  normgt0tOLD 8988  normgt0t 8989  hhsst 9131  occllem4 9171  occllem6 9173  projlem8 9188  projlem13 9193  projlem15 9195  projlem24 9204  projlem25 9205  projlem26 9206  projlem29 9209  pjthlem4 9217  pjthlem7 9220  pjthlem10 9223  pjthlem11 9224  pjthlem12 9225  pjoc1 9259  shlej1 9343  chlejb1 9394  cmbr4 9539  pjjs 9640  adjvalvalt 9856  nmopunt 9934  pjnormss 10091  stge1 10160  stle0 10161  stles 10163  stadd 10168  stadd3 10170  mdsl2b 10245  mdslmd1lem1 10247  faimpex 10433  cdrci 10480  truni1 10485  homindlem2 10536  fgsb 10555  efilcp 10556  fgsb2 10560  cnfilca 10562  dtopcl 10586  dmse1 10594  mslb1 10600  msra3 10602  iintlem1 10603

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