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

Theorem pm3.21 448
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 447 . 2  |-  ( ps 
->  ( ph  ->  ( ps  /\  ph ) ) )
21com12 31 1  |-  ( ph  ->  ( ps  ->  ( ps  /\  ph ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  pm3.22  449  iba  503  ancr  549  anc2r  556  pm5.31  588  19.41  1915  2ax6elem  2172  mo3  2313  2mo  2375  2moOLD  2376  2moOLDOLD  2377  smoord  7026  fisupg  7757  winalim2  9063  relin01  10066  cshwlen  12720  aalioulem5  22459  musum  23188  chrelat2i  26946  waj-ax  29442  pm11.71  30836  ssfz12  31754  onfrALTlem2  32273  19.41rg  32278  not12an2impnot1  32300  onfrALTlem2VD  32644  2pm13.193VD  32658  ax6e2eqVD  32662  bnj1173  33012  hlrelat2  34074
  Copyright terms: Public domain W3C validator