Theorem jctir 317

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 310	1 |- (ph -> (ps /\ ch))

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  equvini 1531  equviniOLD 1532  csbiegf 2575  intminOLD 3238  intab 3247  uniintsn 3253  ordsseleqOLD 3688  ordunidif 3712  funtp 4468  fnprg 4470  fntp 4471  fn0OLD 4533  foimacnv 4657  fpr 4810  curry1 5075  tfrlem10 5128  tz7.44-3 5138  oawordeulem 5236  oelim2 5270  ssdomg 5467  ac6sfilem3 5508  fodomr 5547  limenpsi 5599  phplem4 5605  fodomfi 5656  suppr 5680  supsnALT 5682  ordtype 5691  omsubindss 5888  prlem934a 6289  reclem2pr 6309  recexsrlem 6364  map2psrpr 6372  ltsor 6413  posexi 7091  creur 7992  creui 7993  bcxmas 8336  climeu 8360  arisumilem 8486  arisumi 8487  efaddlem10 8609  efaddlem17 8616  acdc2lem2 8758  acdc5lem2 8761  ruclem33 8811  ruclem35 8813  infxpidmlem7 8827  alephexp2 8855  topbas 8897  neips 9003  blelrn 9125  grpfo 9323  grpidval 9342  ssga 9455  ringideu 9470  nvex 9562  nmcn3 9680  nmcnc 9681  nmosetn0 9767  cdrci 10182  fbunfip 10282  limfil 10297  isfilmap 10308  sflimf 10318  normgt0OLD 10626  normgt0 10627  hhsst 10769  occllem4 10809  occllem6 10811  projlem8 10826  projlem13 10831  projlem15 10833  projlem24 10842  projlem25 10843  projlem26 10844  projlem29 10847  pjthlem4 10855  pjthlem7 10858  pjthlem10 10861  pjthlem11 10862  pjthlem12 10863  pjoc1i 10897  shlej1i 10981  chlejb1i 11032  cmbr4i 11177  pjjsi 11280  adjvalval 11498  nmopun 11576  pjnormssi 11740  stge1i 11810  stle0i 11811  stlesi 11813  staddi 11818  stadd3i 11820  mdsl2bi 11895  mdslmd1lem1 11897  bnj945 12844  bnj103 13223  bnj109 13226  bnj129 13239  bnj522 13261  bnj535 13265  bnj986 13360  bnj1421 13532  algcvgblem 13745  wfrlem13 13969  axdense 14027  axfelem8 14038  nandsym1 14246  repfuntw 14502  prjmapcp2 14515  toplat 14638  fnopabco2b 14734  curgrpact 14735  trooo 14758  ununr 14769  truni1 14849  osneisi 14875  homindlem2 14899  ttcn 14913  fgsb 14921  efilcp 14922  fgsb2 14925  cnfilca 14927  dtopcl 14948  altretop 14997  dmse1 15001  msra3 15009  iintlem1 15010  tarsuc2 15245  ordtypeOLD 15382  omsubindssOLD 15397  opncldf2 15403  subntr 15425  cptclsscpt 15432  compfipin0 15436  reconnlem4 15449  reconnlem5 15450  fness 15491  neibastop2lem1 15519  neibastop2lem3 15521  neibastop2lem4 15522  topmtcl 15525  fnemeet2 15529  fnejoin1 15530  ist1-2 15542  ufinffr 15578  rnelfm 15593  sfcls 15604  filclus 15605  flimfnfcls 15615  sfclusf 15624  tailf 15633  istail 15634  filnetlem3 15642  filnetlem5 15644  respreima 15684  rddif 15798  totbndbnd 15944  heiborlem38 15992  rrntotbnd 16022  phtpcdm 16061  ringideuNEW 17146  paddssat 17275

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 164  df-an 242

Copyright terms: Public domain