![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > jctr | Structured version Visualization version Unicode version |
Description: Inference conjoining a theorem to the right of a consequent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.) |
Ref | Expression |
---|---|
jctl.1 |
![]() ![]() |
Ref | Expression |
---|---|
jctr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | jctl.1 |
. 2
![]() ![]() | |
3 | 1, 2 | jctir 541 |
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 df-an 373 |
This theorem is referenced by: mpanl2 686 mpanr2 689 brprcneu 5856 mpt2eq12 6348 tfr3 7114 oaabslem 7341 omabslem 7344 isinf 7782 pssnn 7787 ige2m2fzo 11974 uzindi 12191 drsdirfi 16176 ga0 16945 lbsext 18379 lindfrn 19372 fbssint 20846 filssufilg 20919 neiflim 20982 lmmbrf 22225 caucfil 22246 constr2spth 25323 constr2pth 25324 constr3lem4 25368 efghgrpOLD 26094 sspid 26357 onsucsuccmpi 31096 poimirlem28 31961 lhpexle1 33567 diophun 35610 eldioph4b 35648 relexp1idm 36300 relexp0idm 36301 dvsid 36674 dvsef 36675 un10 37169 cnfex 37343 dvmptfprod 37814 |
Copyright terms: Public domain | W3C validator |