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 4408  fodomr 4483  limenpsi 4505  phplem4 4511  php 4513  ominfOLD 4529  pssnn 4534  fodomfiOLD 4566  suppr 4590  supsnALT 4592  aceq3lem 4732  aceq6b 4742  cfsuc 4915  prlem934a 5137  reclem2pr 5157  recexsrlem 5212  map2psrpr 5220  supsrlem2 5226  ltsor 5261  posex 5908  nnsub 5956  sqr0 6672  creur 6742  creui 6743  bcxmas 7076  climeu 7100  fnsmntlem 7225  fnsmnt 7226  efaddlem10 7347  efaddlem17 7354  efaddlem23 7360  acdc2lem2 7489  acdc5lem2 7492  ruclem33 7542  ruclem35 7544  infxpidmlem7 7558  infunabs 7565  infcdaabs 7566  alephexp2 7586  topbast 7627  neips 7727  blelrn 7848  grpfo 8043  nvex 8230  nmcn3 8341  nmcnc 8342  nmosetn0 8428  spwpr3OLD 8662  normgt0tOLD 8993  normgt0t 8994  hhsst 9136  occllem4 9176  occllem6 9178  projlem8 9193  projlem13 9198  projlem15 9200  projlem24 9209  projlem25 9210  projlem26 9211  projlem29 9214  pjthlem4 9222  pjthlem7 9225  pjthlem10 9228  pjthlem11 9229  pjthlem12 9230  pjoc1 9264  shlej1 9348  chlejb1 9399  cmbr4 9544  pjjs 9645  adjvalvalt 9861  nmopunt 9939  pjnormss 10096  stge1 10165  stle0 10166  stles 10168  stadd 10173  stadd3 10175  mdsl2b 10250  mdslmd1lem1 10252  faimpex 10438  cdrci 10494  truni1 10499  fgsb 10570  fgsbOLD 10571  efilcp 10572  efilcpOLD 10573  fgsb2 10580  cnfilca 10583  cnfilcaOLD 10584  dtopcl 10615  dmse1 10623  mslb1 10629  msra3 10631  iintlem1 10632

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