MPE Home 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  ad5ant125  1366  3ecase  1474  3elpr2eq  4864  pssnn  9112  pssnnOLD  9209  suppeqfsuppbi  9319  infsupprpr  9440  axdc3lem2  10387  ltexprlem7  10978  nn01to3  12866  xrsupsslem  13226  xrinfmsslem  13227  injresinjlem  13692  injresinj  13693  addmodlteq  13851  ssnn0fi  13890  fsuppmapnn0fiubex  13897  fsuppmapnn0fiub0  13898  nn0o1gt2  16263  cshwsidrepswmod0  16967  symgextf1  19203  psgnunilem4  19279  cmpsublem  22750  aalioulem5  25696  gausslemma2dlem0i  26712  2lgsoddprm  26764  axlowdimlem15  27905  nbusgrvtxm1  28327  nb3grprlem1  28328  lfgrwlkprop  28635  frgrnbnb  29237  frgrwopreglem4a  29254  frgrwopreg  29267  nnn1suc  40768  volicorescl  44784  iccpartiltu  45604  odz2prm2pw  45745  prmdvdsfmtnof1lem2  45767  nnsum3primesle9  45976  bgoldbtbndlem1  45987  lindslinindsimp2lem5  46533  elfzolborelfzop1  46590  nn0sumshdiglemB  46696
  Copyright terms: Public domain W3C validator