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  4906  pssnn  9164  pssnnOLD  9261  suppeqfsuppbi  9373  infsupprpr  9495  axdc3lem2  10442  ltexprlem7  11033  nn01to3  12921  xrsupsslem  13282  xrinfmsslem  13283  injresinjlem  13748  injresinj  13749  addmodlteq  13907  ssnn0fi  13946  fsuppmapnn0fiubex  13953  fsuppmapnn0fiub0  13954  nn0o1gt2  16320  cshwsidrepswmod0  17024  symgextf1  19283  psgnunilem4  19359  cmpsublem  22894  aalioulem5  25840  gausslemma2dlem0i  26856  2lgsoddprm  26908  axlowdimlem15  28203  nbusgrvtxm1  28625  nb3grprlem1  28626  lfgrwlkprop  28933  frgrnbnb  29535  frgrwopreglem4a  29552  frgrwopreg  29565  nnn1suc  41177  volicorescl  45255  iccpartiltu  46076  odz2prm2pw  46217  prmdvdsfmtnof1lem2  46239  nnsum3primesle9  46448  bgoldbtbndlem1  46459  lindslinindsimp2lem5  47096  elfzolborelfzop1  47153  nn0sumshdiglemB  47259
  Copyright terms: Public domain W3C validator