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  1367  3ecase  1475  3elpr2eq  4869  pssnn  9119  pssnnOLD  9216  suppeqfsuppbi  9326  infsupprpr  9447  axdc3lem2  10394  ltexprlem7  10985  nn01to3  12873  xrsupsslem  13233  xrinfmsslem  13234  injresinjlem  13699  injresinj  13700  addmodlteq  13858  ssnn0fi  13897  fsuppmapnn0fiubex  13904  fsuppmapnn0fiub0  13905  nn0o1gt2  16270  cshwsidrepswmod0  16974  symgextf1  19210  psgnunilem4  19286  cmpsublem  22766  aalioulem5  25712  gausslemma2dlem0i  26728  2lgsoddprm  26780  axlowdimlem15  27947  nbusgrvtxm1  28369  nb3grprlem1  28370  lfgrwlkprop  28677  frgrnbnb  29279  frgrwopreglem4a  29296  frgrwopreg  29309  nnn1suc  40811  volicorescl  44868  iccpartiltu  45688  odz2prm2pw  45829  prmdvdsfmtnof1lem2  45851  nnsum3primesle9  46060  bgoldbtbndlem1  46071  lindslinindsimp2lem5  46617  elfzolborelfzop1  46674  nn0sumshdiglemB  46780
  Copyright terms: Public domain W3C validator