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 463
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 462 . 2 (𝜓 → (𝜑 → (𝜓𝜑)))
21com12 32 1 (𝜑 → (𝜓 → (𝜓𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 196  df-an 385
This theorem is referenced by:  pm3.22  464  iba  523  ancr  570  anc2r  577  pm5.31  610  exan  1775  exanOLD  1776  19.29r  1790  19.40b  1804  19.41v  1901  19.41  2090  2ax6elem  2437  mo3  2495  2mo  2539  relopabi  5167  smoord  7349  fisupg  8093  fiinfg  8288  winalim2  9397  relin01  10431  cshwlen  13396  aalioulem5  23895  musum  24717  chrelat2i  28608  bnj1173  30324  waj-ax  31583  hlrelat2  33707  pm11.71  37619  onfrALTlem2  37782  19.41rg  37787  not12an2impnot1  37805  onfrALTlem2VD  38147  2pm13.193VD  38161  ax6e2eqVD  38165  ssfz12  40351
  Copyright terms: Public domain W3C validator