Theorem pm3.35 587

Description: Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112. (Contributed by NM, 14-Dec-2002.)

Assertion

Ref	Expression
pm3.35

Proof of Theorem pm3.35

Step	Hyp	Ref	Expression
1		pm2.27 39	. 2
2	1	imp 429	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  ornld  898  r19.29af2OLD  2996  r19.29_2a  3001  2reu5  3308  intab  4317  dfac5  8530  grothpw  9225  grothpwex  9226  gcdcllem1  14149  gsmsymgreqlem2  16456  neindisj2  19624  tx1stc  20151  ufinffr  20430  ucnima  20784  fmcncfil  27913  sgn3da  28480  itg2gt0cn  30070  unirep  30203  ispridl2  30435  cnf1dd  30490  impel  30503  fmul01  31574  dvnmptconst  31738  dvnmul  31740  unisnALT  33726  ax6e2ndALT  33730  bnj605  33965  bnj594  33970  bnj1174  34059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371