Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3adant3r1 | Structured version Visualization version Unicode version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.) |
Ref | Expression |
---|---|
3exp.1 |
Ref | Expression |
---|---|
3adant3r1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 | |
2 | 1 | 3expb 1266 | . 2 |
3 | 2 | 3adantr1 1220 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: plttr 16970 pltletr 16971 latjlej1 17065 latjlej2 17066 latnlej 17068 latnlej2 17071 latmlem2 17082 latledi 17089 latjass 17095 latj32 17097 latj13 17098 ipopos 17160 tsrlemax 17220 imasmnd2 17327 grpsubsub 17504 grpnnncan2 17512 imasgrp2 17530 mulgnn0ass 17578 mulgsubdir 17582 cmn32 18211 ablsubadd 18217 imasring 18619 zntoslem 19905 xmettri3 22158 mettri3 22159 xmetrtri 22160 xmetrtri2 22161 metrtri 22162 cphdivcl 22982 cphassr 23012 relogbmulexp 24516 grpodivdiv 27394 grpomuldivass 27395 ablo32 27403 ablodivdiv4 27408 ablodiv32 27409 ablonnncan 27410 nvmdi 27503 dipdi 27698 dipassr 27701 dipsubdir 27703 dipsubdi 27704 dvrcan5 29793 cgr3tr4 32159 cgr3rflx 32161 endofsegid 32192 seglemin 32220 broutsideof2 32229 rngosubdi 33744 rngosubdir 33745 isdrngo2 33757 crngm23 33801 dmncan2 33876 latmassOLD 34516 latm32 34518 cvrnbtwn4 34566 cvrcmp2 34571 ltcvrntr 34710 atcvrj0 34714 3dim3 34755 paddasslem17 35122 paddass 35124 lautlt 35377 lautcvr 35378 lautj 35379 lautm 35380 erngdvlem3 36278 dvalveclem 36314 mendlmod 37763 |
Copyright terms: Public domain | W3C validator |