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  1363  3ecase  1471  3elpr2eq  4800  supp0cosupp0OLD  7859  imacosuppOLD  7861  pssnn  8723  suppeqfsuppbi  8834  infsupprpr  8955  axdc3lem2  9865  ltexprlem7  10456  nn01to3  12332  xrsupsslem  12691  xrinfmsslem  12692  injresinjlem  13155  injresinj  13156  addmodlteq  13312  ssnn0fi  13351  fsuppmapnn0fiubex  13358  fsuppmapnn0fiub0  13359  nn0o1gt2  15725  cshwsidrepswmod0  16423  symgextf1  18545  psgnunilem4  18621  cmpsublem  22014  aalioulem5  24942  gausslemma2dlem0i  25958  2lgsoddprm  26010  axlowdimlem15  26760  nbusgrvtxm1  27179  nb3grprlem1  27180  lfgrwlkprop  27487  frgrnbnb  28088  frgrwopreglem4a  28105  frgrwopreg  28118  nnn1suc  39510  volicorescl  43235  iccpartiltu  43982  odz2prm2pw  44123  prmdvdsfmtnof1lem2  44145  nnsum3primesle9  44355  bgoldbtbndlem1  44366  lindslinindsimp2lem5  44912  elfzolborelfzop1  44969  nn0sumshdiglemB  45075
 Copyright terms: Public domain W3C validator