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  ad4ant14  1290  ad5ant145  1312  3ecase  1434  supp0cosupp0  7286  imacosupp  7287  pssnn  8130  suppeqfsuppbi  8241  axdc3lem2  9225  ltexprlem7  9816  xrsupsslem  12088  xrinfmsslem  12089  injresinjlem  12536  injresinj  12537  addmodlteq  12693  ssnn0fi  12732  fsuppmapnn0fiubex  12740  fsuppmapnn0fiub0  12741  nn0o1gt2  15032  cshwsidrepswmod0  15736  symgextf1  17773  psgnunilem4  17849  cmpsublem  21125  aalioulem5  24012  gausslemma2dlem0i  25006  2lgsoddprm  25058  axlowdimlem15  25753  nbusgrvtxm1  26185  nb3grprlem1  26186  lfgrwlkprop  26470  frgrnbnb  27038  frgrwopreglem4  27059  numclwwlkffin0  27088  volicorescl  40100  iccpartiltu  40682  odz2prm2pw  40800  prmdvdsfmtnof1lem2  40822  nnsum3primesle9  40997  bgoldbtbndlem1  41008  lindslinindsimp2lem5  41565  elfzolborelfzop1  41623  nn0sumshdiglemB  41732
 Copyright terms: Public domain W3C validator