![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2thd | Structured version Visualization version Unicode version |
Description: Two truths are equivalent (deduction rule). (Contributed by NM, 3-Jun-2012.) |
Ref | Expression |
---|---|
2thd.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
2thd.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
2thd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2thd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 2thd.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | pm5.1im 242 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | sylc 62 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 189 |
This theorem is referenced by: sbc2or 3275 abvor0 3749 ralidm 3872 disjprg 4397 euotd 4701 posn 4902 frsn 4904 cnvpo 5373 elabrex 6146 riota5f 6274 smoord 7081 brwdom2 8085 finacn 8478 acacni 8567 dfac13 8569 fin1a2lem10 8836 gch2 9097 gchac 9103 recmulnq 9386 nn1m1nn 10626 nn0sub 10917 qextltlem 11492 xsubge0 11544 xlesubadd 11546 iccshftr 11763 iccshftl 11765 iccdil 11767 icccntr 11769 fzaddel 11830 elfzomelpfzo 12010 sqlecan 12378 nnesq 12393 hashdom 12555 swrdspsleq 12800 repswsymballbi 12878 znnenlem 14257 bitsmod 14403 dvdssq 14521 pcdvdsb 14811 vdwmc2 14922 acsfn 15558 subsubc 15751 funcres2b 15795 isipodrs 16400 issubg3 16828 opnnei 20129 lmss 20307 lmres 20309 cmpfi 20416 xkopt 20663 acufl 20925 lmhmclm 22110 equivcmet 22278 degltlem1 23014 mdegle0 23019 cxple2 23635 rlimcnp3 23886 dchrelbas3 24159 tgcolg 24592 hlbtwn 24649 eupath2lem3 25700 isoun 28275 smatrcl 28615 msrrcl 30174 fz0n 30357 onint1 31102 bj-nfcsym 31487 ftc1anclem6 32015 lcvexchlem1 32594 ltrnatb 33696 cdlemg27b 34257 gicabl 35951 dfacbasgrp 35961 sdrgacs 36061 rp-fakeimass 36150 radcnvrat 36657 elabrexg 37364 eliooshift 37598 ellimcabssub0 37691 |
Copyright terms: Public domain | W3C validator |