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  1358  3ecase  1465  3elpr2eq  4829  supp0cosupp0OLD  7862  imacosuppOLD  7864  pssnn  8724  suppeqfsuppbi  8835  infsupprpr  8956  axdc3lem2  9861  ltexprlem7  10452  nn01to3  12329  xrsupsslem  12688  xrinfmsslem  12689  injresinjlem  13145  injresinj  13146  addmodlteq  13302  ssnn0fi  13341  fsuppmapnn0fiubex  13348  fsuppmapnn0fiub0  13349  nn0o1gt2  15720  cshwsidrepswmod0  16416  symgextf1  18478  psgnunilem4  18554  cmpsublem  21935  aalioulem5  24852  gausslemma2dlem0i  25867  2lgsoddprm  25919  axlowdimlem15  26669  nbusgrvtxm1  27088  nb3grprlem1  27089  lfgrwlkprop  27396  frgrnbnb  27999  frgrwopreglem4a  28016  frgrwopreg  28029  nnn1suc  39037  volicorescl  42712  iccpartiltu  43459  odz2prm2pw  43602  prmdvdsfmtnof1lem2  43624  nnsum3primesle9  43836  bgoldbtbndlem1  43847  lindslinindsimp2lem5  44445  elfzolborelfzop1  44502  nn0sumshdiglemB  44608
  Copyright terms: Public domain W3C validator