MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm3.21 Structured version   Unicode version

Theorem pm3.21 446
Description: Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
pm3.21  |-  ( ph  ->  ( ps  ->  ( ps  /\  ph ) ) )

Proof of Theorem pm3.21
StepHypRef Expression
1 pm3.2 445 . 2  |-  ( ps 
->  ( ph  ->  ( ps  /\  ph ) ) )
21com12 29 1  |-  ( ph  ->  ( ps  ->  ( ps  /\  ph ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  pm3.22  447  iba  501  ancr  547  anc2r  554  pm5.31  586  19.41v  1795  19.41  1999  2ax6elem  2217  mo3  2278  2mo  2324  2moOLD  2325  smoord  7068  fisupg  7801  winalim2  9103  relin01  10116  cshwlen  12824  aalioulem5  23022  musum  23846  chrelat2i  27683  bnj1173  29372  waj-ax  30633  hlrelat2  32400  pm11.71  36131  onfrALTlem2  36322  19.41rg  36327  not12an2impnot1  36349  onfrALTlem2VD  36700  2pm13.193VD  36714  ax6e2eqVD  36718  ssfz12  37943
  Copyright terms: Public domain W3C validator