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

Theorem pm3.21 464
Description: Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
pm3.21 (𝜑 → (𝜓 → (𝜓𝜑)))

Proof of Theorem pm3.21
StepHypRef Expression
1 pm3.2 463 . 2 (𝜓 → (𝜑 → (𝜓𝜑)))
21com12 32 1 (𝜑 → (𝜓 → (𝜓𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  pm3.22  465  iba  524  ancr  571  anc2r  578  pm5.31  611  exan  1785  exanOLD  1786  19.29r  1799  19.40b  1812  19.41v  1911  19.41  2101  2ax6elem  2448  mo3  2506  2mo  2550  relopabi  5205  smoord  7407  fisupg  8152  fiinfg  8349  winalim2  9462  relin01  10496  cshwlen  13482  aalioulem5  23995  musum  24817  chrelat2i  29070  bnj1173  30775  waj-ax  32052  hlrelat2  34166  pm11.71  38076  onfrALTlem2  38240  19.41rg  38245  not12an2impnot1  38263  onfrALTlem2VD  38605  2pm13.193VD  38619  ax6e2eqVD  38623  ssfz12  40618
  Copyright terms: Public domain W3C validator