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  1360  3ecase  1467  3elpr2eq  4835  supp0cosupp0OLD  7867  imacosuppOLD  7869  pssnn  8728  suppeqfsuppbi  8839  infsupprpr  8960  axdc3lem2  9865  ltexprlem7  10456  nn01to3  12333  xrsupsslem  12693  xrinfmsslem  12694  injresinjlem  13150  injresinj  13151  addmodlteq  13307  ssnn0fi  13346  fsuppmapnn0fiubex  13353  fsuppmapnn0fiub0  13354  nn0o1gt2  15724  cshwsidrepswmod0  16420  symgextf1  18471  psgnunilem4  18547  cmpsublem  21923  aalioulem5  24840  gausslemma2dlem0i  25854  2lgsoddprm  25906  axlowdimlem15  26656  nbusgrvtxm1  27075  nb3grprlem1  27076  lfgrwlkprop  27383  frgrnbnb  27986  frgrwopreglem4a  28003  frgrwopreg  28016  nnn1suc  39022  volicorescl  42697  iccpartiltu  43410  odz2prm2pw  43553  prmdvdsfmtnof1lem2  43575  nnsum3primesle9  43787  bgoldbtbndlem1  43798  lindslinindsimp2lem5  44345  elfzolborelfzop1  44402  nn0sumshdiglemB  44508
  Copyright terms: Public domain W3C validator