Theorem jctir 291

Description: Inference conjoining a theorem to right of consequent in an implication.

Hypotheses

Ref	Expression
jctir.1	⊢ (φ → ψ)
jctir.2	⊢ χ

Assertion

Ref	Expression
jctir	⊢ (φ → (ψ ⋀ χ))

Proof of Theorem jctir

Step	Hyp	Ref	Expression
1		jctir.1	. 2 ⊢ (φ → ψ)
2		jctir.2	. . 3 ⊢ χ
3	2	a1i 8	. 2 ⊢ (φ → χ)
4	1, 3	jca 286	1 ⊢ (φ → (ψ ⋀ χ))

Syntax hints:   → wi 3   ⋀ wa 221

This theorem is referenced by:  equvini 1205  csbiegf 2083  intmin 2620  intab 2627  ordsseleq 3004  ordunidif 3022  onssmin 3154  fn0 3711  foimacnv 3814  dffn5 3869  fsn 3948  curry1 4193  tfrlem10 4221  tz7.44-3 4231  oawordeulem 4324  oelim2 4358  ixp0 4502  ssdomg 4549  ac6sfilem3 4590  fodomr 4628  limenpsi 4652  phplem4 4658  php 4660  ominf 4675  pssnn 4681  fodomfi 4709  suppr 4733  supsnALT 4735  aceq3lem 4878  aceq6b 4888  cfsuc 5065  prlem934a 5291  reclem2pr 5311  recexsrlem 5366  map2psrpr 5374  supsrlem2 5380  ltsor 5415  posexi 6053  nnsubi 6102  sqr0 6873  creur 6943  creui 6944  bcxmas 7279  climeu 7303  arisumilem 7429  arisumi 7430  efaddlem10 7552  efaddlem17 7559  acdc2lem2 7701  acdc5lem2 7704  ruclem33 7754  ruclem35 7756  infxpidmlem7 7770  infunabs 7777  infcdaabs 7778  alephexp2 7798  topbas 7839  neips 7937  blelrn 8058  grpfo 8256  grpidval 8275  ringideu 8387  nvex 8477  nmcn3 8595  nmcnc 8596  nmosetn0 8682  normgt0OLD 9269  normgt0 9270  hhsst 9412  occllem4 9452  occllem6 9454  projlem8 9469  projlem13 9474  projlem15 9476  projlem24 9485  projlem25 9486  projlem26 9487  projlem29 9490  pjthlem4 9498  pjthlem7 9501  pjthlem10 9504  pjthlem11 9505  pjthlem12 9506  pjoc1i 9540  shlej1i 9624  chlejb1i 9675  cmbr4i 9820  pjjsi 9923  adjvalval 10141  nmopun 10218  pjnormssi 10376  stge1i 10446  stle0i 10447  stlesi 10449  staddi 10454  stadd3i 10456  mdsl2bi 10531  mdslmd1lem1 10533  toplat 10884  ununr 10955  cdrci 10994  truni1 10999  osneisi 11018  homindlem2 11052  fgsb 11082  efilcp 11083  fgsb2 11086  cnfilca 11088  dtopcl 11107  altretop 11144  dmse1 11146  msra3 11154  iintlem1 11155  ordtype 11434  omsubindss 11449  opncldf2 11455  subntr 11482  cptclsscpt 11489  compfipin0 11493  reconnlem4 11510  reconnlem5 11511  fness 11552  neibastop2lem1 11580  neibastop2lem3 11582  neibastop2lem4 11583  topmtcl 11586  fnemeet2 11590  fnejoin1 11591  ist1-2 11603  fbunfip 11631  ufinffr 11663  limfil 11675  isfilmap 11689  rnelfm 11699  sflimf 11708  sfcls 11716  filclus 11717  flimfnfcls 11727  sfclusf 11736  tailf 11756  istail 11757  filnetlem3 11765  filnetlem5 11767  ssga 11777  respreima 11795  rddif 11869  totbndbnd 12000  heiborlem38 12048  rrntotbnd 12078  phtpcdm 12103

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 145  df-an 223

Copyright terms: Public domain