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 472
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 id 22 . 2 ((𝜓𝜑) → (𝜓𝜑))
21expcom 414 1 (𝜑 → (𝜓 → (𝜓𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  iba  528  ancr  547  anc2r  555  19.29r  1866  19.40b  1880  19.41v  1941  19.41  2227  2ax6elem  2485  mo3  2641  2mo  2726  relopabi  5687  smoord  7991  fisupg  8754  winalim2  10106  relin01  11152  cshwlen  14149  aalioulem5  24852  musum  25695  chrelat2i  30069  bnj1173  32171  waj-ax  33659  hlrelat2  36419  pm11.71  40606  onfrALTlem2  40757  19.41rg  40761  not12an2impnot1  40779  onfrALTlem2VD  41100  2pm13.193VD  41114  ax6e2eqVD  41118  ssfz12  43391
  Copyright terms: Public domain W3C validator