![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2a1d | Structured version Visualization version GIF version |
Description: Deduction introducing two antecedents. Two applications of a1d 25. Deduction associated with 2a1 28 and 2a1i 12. (Contributed by BJ, 10-Aug-2020.) |
Ref | Expression |
---|---|
2a1d.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
2a1d | ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2a1d.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | a1d 25 | . 2 ⊢ (𝜑 → (𝜃 → 𝜓)) |
3 | 2 | a1d 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 |