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 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 |