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

Theorem 2a1d 26
 Description: Deduction introducing two antecedents. Two applications of a1d 25. Deduction associated with 2a1 28 and 2a1i 12. (Contributed by BJ, 10-Aug-2020.)
Hypothesis
Ref Expression
2a1d.1 (𝜑𝜓)
Assertion
Ref Expression
2a1d (𝜑 → (𝜒 → (𝜃𝜓)))

Proof of Theorem 2a1d
StepHypRef Expression
1 2a1d.1 . . 3 (𝜑𝜓)
21a1d 25 . 2 (𝜑 → (𝜃𝜓))
32a1d 25 1 (𝜑 → (𝜒 → (𝜃𝜓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7 This theorem is referenced by:  2a1  28  ad4ant14OLD  1318  ad5ant145  1355  3ecase  1477  3elpr2eq  4467  supp0cosupp0  7379  imacosupp  7380  pssnn  8219  suppeqfsuppbi  8330  axdc3lem2  9311  ltexprlem7  9902  xrsupsslem  12175  xrinfmsslem  12176  injresinjlem  12628  injresinj  12629  addmodlteq  12785  ssnn0fi  12824  fsuppmapnn0fiubex  12832  fsuppmapnn0fiub0  12833  nn0o1gt2  15144  cshwsidrepswmod0  15848  symgextf1  17887  psgnunilem4  17963  cmpsublem  21250  aalioulem5  24136  gausslemma2dlem0i  25134  2lgsoddprm  25186  axlowdimlem15  25881  nbusgrvtxm1  26325  nb3grprlem1  26326  lfgrwlkprop  26640  frgrnbnb  27273  frgrwopreglem4a  27290  frgrwopreg  27303  volicorescl  41088  iccpartiltu  41683  odz2prm2pw  41800  prmdvdsfmtnof1lem2  41822  nnsum3primesle9  42007  bgoldbtbndlem1  42018  lindslinindsimp2lem5  42576  elfzolborelfzop1  42634  nn0sumshdiglemB  42739
 Copyright terms: Public domain W3C validator