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  ad4ant14OLD  761  ad5ant125  1481  ad5ant145OLD  1488  3ecase  1599  3elpr2eq  4628  supp0cosupp0  7573  imacosupp  7574  pssnn  8421  suppeqfsuppbi  8532  axdc3lem2  9562  ltexprlem7  10153  xrsupsslem  12385  xrinfmsslem  12386  injresinjlem  12842  injresinj  12843  addmodlteq  12999  ssnn0fi  13038  fsuppmapnn0fiubex  13045  fsuppmapnn0fiub0  13046  nn0o1gt2  15432  cshwsidrepswmod0  16128  symgextf1  18152  psgnunilem4  18229  cmpsublem  21530  aalioulem5  24431  gausslemma2dlem0i  25440  2lgsoddprm  25492  axlowdimlem15  26192  nbusgrvtxm1  26622  nb3grprlem1  26623  lfgrwlkprop  26939  frgrnbnb  27641  frgrwopreglem4a  27658  frgrwopreg  27671  volicorescl  41508  iccpartiltu  42193  odz2prm2pw  42252  prmdvdsfmtnof1lem2  42274  nnsum3primesle9  42459  bgoldbtbndlem1  42470  lindslinindsimp2lem5  43045  elfzolborelfzop1  43103  nn0sumshdiglemB  43208
  Copyright terms: Public domain W3C validator