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

Theorem pm3.21 449
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 448 . 2  |-  ( ps 
->  ( ph  ->  ( ps  /\  ph ) ) )
21com12 32 1  |-  ( ph  ->  ( ps  ->  ( ps  /\  ph ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  pm3.22  450  iba  505  ancr  551  anc2r  558  pm5.31  590  19.41v  1819  19.41  2026  2ax6elem  2244  mo3  2303  2mo  2347  2moOLD  2348  smoord  7089  fisupg  7822  fiinfg  8018  winalim2  9122  relin01  10139  cshwlen  12892  aalioulem5  23279  musum  24107  chrelat2i  28004  bnj1173  29807  waj-ax  31067  hlrelat2  32887  pm11.71  36605  onfrALTlem2  36770  19.41rg  36775  not12an2impnot1  36797  onfrALTlem2VD  37147  2pm13.193VD  37161  ax6e2eqVD  37165  ssfz12  38743
  Copyright terms: Public domain W3C validator